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