theorem :: ORDINAL3:55

for A, B being Ordinal st A in B holds
( B -^ A <> {} & {} in B -^ A )