let A, B be Ordinal; :: thesis: ( A c= A +^ B & B c= A +^ B )
A1: {} +^ B c= A +^ B by ORDINAL2:34, XBOOLE_1:2;
A +^ {} c= A +^ B by ORDINAL2:33, XBOOLE_1:2;
hence ( A c= A +^ B & B c= A +^ B ) by A1, ORDINAL2:27, ORDINAL2:30; :: thesis: verum