let Nseq be increasing sequence of NAT; :: thesis: for n being Nat holds n <= Nseq . n
defpred S₁[ Nat] means $1 <= Nseq . $1;

A1: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A2: S₁[k] ; :: thesis: S₁[k + 1]
Nseq . k < Nseq . (k + 1) by Lm7;
then k < Nseq . (k + 1) by A2, XXREAL_0:2;
hence S₁[k + 1] by NAT_1:13; :: thesis: verum

end;

A3: S₁[ 0 ] ;
thus for k being Nat holds S₁[k] from NAT_1:sch 2(A3, A1); :: thesis: verum