theorem Th63: :: CLASSES1:63

for X being set holds the_rank_of (bool X) = succ (the_rank_of X)