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

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

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 Def5; :: thesis: verum

end;

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

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

end;

end;

end;

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