theorem :: CLASSES1:40

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