let i, j be Nat; :: thesis: ( not i <= j + 1 or i <= j or i = j + 1 )
defpred S₁[ Nat] means for j being Nat holds
( not $1 <= j + 1 or $1 <= j or $1 = j + 1 );
A1: S₁[ 0 ] by Th2;
A2: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A3: for j being Nat holds
( not i <= j + 1 or i <= j or i = j + 1 ) ; :: thesis: S₁[i + 1]
let j be Nat; :: thesis: ( not i + 1 <= j + 1 or i + 1 <= j or i + 1 = j + 1 )
assume A4: i + 1 <= j + 1 ; :: thesis: ( i + 1 <= j or i + 1 = j + 1 )

A5: now

assume A6: j = 0 ; :: thesis: ( i + 1 <= j or i + 1 = j + 1 )
then A7: i <= 0 by A4, XREAL_1:8;
0 <= i by Th2;
hence ( i + 1 <= j or i + 1 = j + 1 ) by A6, A7; :: thesis: verum

end;

now

given k being Nat such that A8: j = k + 1 ; :: thesis: ( i + 1 <= j or i + 1 = j + 1 )
i <= k + 1 by A4, A8, XREAL_1:8;
then ( i <= k or i = k + 1 ) by A3;
hence ( i + 1 <= j or i + 1 = j + 1 ) by A8, XREAL_1:8; :: thesis: verum

end;

hence ( i + 1 <= j or i + 1 = j + 1 ) by A5, Th6; :: thesis: verum

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(A1, A2);
hence ( not i <= j + 1 or i <= j or i = j + 1 ) ; :: thesis: verum