theorem Th43: :: CLASSES1:43

for x being set
for A being Ordinal holds
( x in Rank A iff {x} in Rank (succ A) )