theorem Th35: :: ORDINAL3:35
for A, B, C being Ordinal st B *^ A c= C *^ A & A <> {} holds
B c= C