let n be Element of NAT ; :: thesis: Rank n is finite
defpred S2[ Element of NAT ] means Rank $1 is finite ;
A1: S2[ 0 ] by CLASSES1:33;
A2: for n being Element of NAT st S2[n] holds
S2[n + 1] by Lm1;
for n being Element of NAT holds S2[n] from NAT_1:sch 1(A1, A2);
 hence Rank n is finite ; :: thesis: verum