let n be natural number ; :: thesis: ( Rank n is finite implies Rank (n + 1) is finite )
n + 1 = succ n by NAT_1:38;
then Rank (n + 1) = bool (Rank n) by CLASSES1:30;
hence ( Rank n is finite implies Rank (n + 1) is finite ) ; :: thesis: verum