theorem Th36: :: ORDINAL3:36
for A, B being Ordinal st B <> {} holds
( A c= A *^ B & A c= B *^ A )