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