theorem Th12: :: ORDINAL1:16

for A, B being Ordinal holds
( A c= B or B in A )