theorem Th8: :: ORDINAL3:8

for A being Ordinal st A <> {} holds
{} in A