defpred S₁[ Nat] means for m, l being Nat st $1 <= l & l <= m & not $1 = l holds
( $1 + 1 <= l & l <= m );
A1: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume S₁[k] ; :: thesis: S₁[k + 1]
let m, l be Nat; :: thesis: ( k + 1 <= l & l <= m & not k + 1 = l implies ( (k + 1) + 1 <= l & l <= m ) )
assume that
A2: k + 1 <= l and
A3: l <= m ; :: thesis: ( k + 1 = l or ( (k + 1) + 1 <= l & l <= m ) )
( k + 1 = l or k + 1 < l ) by A2, XXREAL_0:1;
hence ( k + 1 = l or ( (k + 1) + 1 <= l & l <= m ) ) by A3, NAT_1:13; :: thesis: verum

end;

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