theorem Th42: :: CLASSES1:42

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