theorem Th53: :: ORDINAL3:53
for A, B, C being Ordinal st A in B & ( C c= A or C in A ) holds
A -^ C in B -^ C