defpred S1[ 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 S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume
S1[
k]
;
S1[k + 1]
let m,
l be
Nat;
( 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
;
( 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;
verum
end;
A4:
S1[ 0 ]
by NAT_1:13;
thus
for k being Nat holds S1[k]
from NAT_1:sch 2(A4, A1); verum