let n be Element of NAT ; :: thesis: ( Rank n is finite implies Rank (n + 1) is finite )
n + 1 = succ n by NAT_1:39;
then Rank (n + 1) = bool (Rank n) by CLASSES1:34;
hence ( Rank n is finite implies Rank (n + 1) is finite ) ; :: thesis: verum