let A, B be Ordinal; :: thesis: ( A c= A +^ B & B c= A +^ B )
( {} c= A & {} c= B ) by XBOOLE_1:2;
then ( A +^ {} c= A +^ B & {} +^ B c= A +^ B & A +^ {} = A & {} +^ B = B ) by ORDINAL2:44, ORDINAL2:47, ORDINAL2:50, ORDINAL2:51;
hence ( A c= A +^ B & B c= A +^ B ) ; :: thesis: verum