theorem Th28: :: ORDINAL3:28

for A, B being Ordinal st A in B holds
ex C being Ordinal st
( B = A +^ C & C <> {} )