theorem Th19: :: ORDINAL3:19
for A, B, C, D being Ordinal st A in B & ( ( C c= D & D <> {} ) or C in D ) holds
A *^ C in B *^ D