theorem Th16: :: ORDINAL3:16

for A being Ordinal holds
( not A c= 1 or A = {} or A = 1 )