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

now

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 Def6;
then A = B +^ (C +^ (A -^ (B +^ C))) by Th33;
then C +^ (A -^ (B +^ C)) = A -^ B by Th65;
hence A -^ (B +^ C) = (A -^ B) -^ C by Th65; :: thesis: verum

end;

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

A2: now

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

end;

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

end;

end;

end;

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