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 A1: not B c= A ; :: thesis: A c= B +^ (A -^ B)

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

end;

end;

end;

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