theorem Th32: :: CLASSES1:32

for X being set
for A being Ordinal holds
( X c= Rank A iff X in Rank (succ A) )