environ
    given glass being CONTAINER;
    given juice being DRINK;
    A1: Full[glass] implies Fresh[juice];
    A2: not Fresh[juice];
begin       == We show that: not Full[glass]

== The proof version

    not Full[glass] proof                 == NI
        assume A: Full[glass];
               1: Fresh[juice] by A, A1;  == IE
        thus contradiction by 1,A2;       == ContrI
    end;

== The now version

   S: now
        assume A: Full[glass];
               1: Fresh[juice] by A, A1;  == IE
        thus contradiction by 1,A2;       == ContrI
    end;
    not Full[glass] by S                  == NI