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

now

per cases ( B c= A or not B c= A ) ;

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

hence A c= B +^ (A -^ B) by Def6; :: thesis: verum

end;

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

then ( A -^ B = {} & A in B & B +^ {} = B ) by Def6, ORDINAL1:26, ORDINAL2:44;
hence A c= B +^ (A -^ B) by ORDINAL1:def 2; :: thesis: verum

end;

end;

end;

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