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