let n be Nat; :: thesis: Rank n is finite
defpred S₁[ Nat] means Rank $1 is finite ;
A1: S₁[ 0 ] by CLASSES1:29;
A2: for n being Nat st S₁[n] holds
S₁[n + 1] by Lm7;
for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A2);
hence Rank n is finite ; :: thesis: verum