environ
    given S being STUDENT;
    given M being Money;
begin
    (Need[M] implies Work[S] & Save[M]) 
        implies 
    (Need[M] implies Work[S]) & (not Save[M] implies not Need[M])
    proof                                                             == II
        assume A:( Need[M] implies Work[S] & Save[M] );

== At this point we have to prove the consequent of the original formula.
== It is a conjunction. The first conjunct is concluded by a thus.

        thus Need[M] implies Work[S] proof                            == II
               assume A1: Need[M];
                      1a: Work[S] & Save[M] by A, A1;                 == IE
               thus Work[S] by 1a;                                    == CE
           end;

== At this point the second conjunct has to be concluded. 
== Since it is an implication we incorporate the proof of the implication
== into the main proof.
== We are really doing the implication introduction from here on.

        assume A1: not Save[M];
 
== What remains to be proven at this point is: not Need[M]

               2a: now                                                == II
                    assume A2: Need[M];
                           2b: Work[S] & Save[M] by A, A2;            == IE
                    thus Save[M] by 2b;                               == CE
               end;

        thus not Need[M] by A1, 2a;                                   == MT
    end;