environ
    given glass being CONTAINER;
begin  == We will demonstrate that the following weird formula is always true:
       ==         (not Full[glass] implies Full[glass]) implies Full[glass]

    1: now
        assume a: not Full[glass] implies Full[glass];
               S: now    == We prepare for Negation Introduction
                    assume b: not Full[glass];
                           c: Full[glass] by a, b;            == MP
                    thus contradiction by c, b;               == ContrI
                  end;

               d: not not Full[glass] by S;                   == NI
        thus Full[glass] by d                                 == NE
    end;

    (not Full[glass] implies Full[glass]) implies Full[glass] by 1; == II