let n be Nat; :: thesis: ( Rank n is finite implies Rank (n + 1) is finite )
Segm (n + 1) = succ (Segm 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