theorem :: CLASSES1:30

for A being Ordinal holds Rank (succ A) = bool (Rank A) by Lm2;