let B, A be Ordinal; :: thesis: ( B <> {} implies ( A c= A *^ B & A c= B *^ A ) )
assume B <> {} ; :: thesis: ( A c= A *^ B & A c= B *^ A )
then {} in B by Th10;
then 1 c= B by Lm1, ORDINAL1:33;
then ( 1 *^ A c= B *^ A & A *^ 1 c= A *^ B & A *^ 1 = A & 1 *^ A = A ) by ORDINAL2:56, ORDINAL2:58, ORDINAL2:59;
hence ( A c= A *^ B & A c= B *^ A ) ; :: thesis: verum