let i, j be natural Number ; :: thesis: ( i <= j implies ex k being Nat st j = i + k )
A0: j is Nat by TARSKI:1;
defpred S₁[ Nat] means ( i <= $1 implies ex k being Nat st $1 = i + k );
A1: for j being Nat st S₁[j] holds
S₁[j + 1]

proof

let j be Nat; :: thesis: ( S₁[j] implies S₁[j + 1] )
assume A2: ( i <= j implies ex k being Nat st j = i + k ) ; :: thesis: S₁[j + 1]

A3: now :: thesis: ( i <= j implies S₁[j + 1] )

assume i <= j ; :: thesis: S₁[j + 1]
then consider k being Nat such that
A4: j = i + k by A2;
(i + k) + 1 = i + (k + 1) ;
hence S₁[j + 1] by A4; :: thesis: verum

end;

A5: now :: thesis: ( i = j + 1 implies S₁[j + 1] )

assume i = j + 1 ; :: thesis: S₁[j + 1]
then j + 1 = i + 0 ;
hence S₁[j + 1] ; :: thesis: verum

end;

assume i <= j + 1 ; :: thesis: ex k being Nat st j + 1 = i + k
hence ex k being Nat st j + 1 = i + k by A3, A5, Th8; :: thesis: verum

end;

A6: S₁[ 0 ]

proof

assume A7: i <= 0 ; :: thesis: ex k being Nat st 0 = i + k
take 0 ; :: thesis: 0 = i + 0
thus 0 = i + 0 by A7, Th2; :: thesis: verum

end;

for j being Nat holds S₁[j] from NAT_1:sch 2(A6, A1);
hence ( i <= j implies ex k being Nat st j = i + k ) by A0; :: thesis: verum