let A, B, C be Ordinal; :: thesis: A -^ (B +^ C) = (A -^ B) -^ C

now :: thesis: A -^ (B +^ C) = (A -^ B) -^ C

per cases ( B +^ C c= A or not B +^ C c= A ) ;

suppose B +^ C c= A ; :: thesis: A -^ (B +^ C) = (A -^ B) -^ C

then A = (B +^ C) +^ (A -^ (B +^ C)) by Def5;
then A = B +^ (C +^ (A -^ (B +^ C))) by Th30;
then C +^ (A -^ (B +^ C)) = A -^ B by Th52;
hence A -^ (B +^ C) = (A -^ B) -^ C by Th52; :: thesis: verum

end;

suppose A1: not B +^ C c= A ; :: thesis: A -^ (B +^ C) = (A -^ B) -^ C

A2: now :: thesis: ( A = B +^ (A -^ B) implies (A -^ B) -^ C = {} )

assume A = B +^ (A -^ B) ; :: thesis: (A -^ B) -^ C = {}
then not C c= A -^ B by A1, ORDINAL2:33;
hence (A -^ B) -^ C = {} by Def5; :: thesis: verum

end;

( B c= A or not B c= A ) ;
then A3: ( A = B +^ (A -^ B) or A -^ B = {} ) by Def5;
A -^ (B +^ C) = {} by A1, Def5;
hence A -^ (B +^ C) = (A -^ B) -^ C by A3, A2, Th56; :: thesis: verum

end;

end;

end;

hence A -^ (B +^ C) = (A -^ B) -^ C ; :: thesis: verum