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.
== Since it is a conjunction, we do it in two separate thus'es.

        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;

        thus not Save[M] implies not Need[M] proof                    == II
              assume A1: not Save[M];
                     2a: Need[M] implies Save[M] proof                == 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;
    end;