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