let i, j be natural Number ; :: thesis: ( not i <= j + 1 or i <= j or i = j + 1 )
A0: ( i is Nat & j is Nat ) by TARSKI:1;
defpred S1[ natural Number ] means for j being Nat holds
( not $1 <= j + 1 or $1 <= j or $1 = j + 1 );
A1: for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be Nat; :: thesis: ( S1[i] implies S1[i + 1] )
assume A2: for j being Nat holds
( not i <= j + 1 or i <= j or i = j + 1 ) ; :: thesis: S1[i + 1]
let j be Nat; :: thesis: ( not i + 1 <= j + 1 or i + 1 <= j or i + 1 = j + 1 )
assume A3: i + 1 <= j + 1 ; :: thesis: ( i + 1 <= j or i + 1 = j + 1 )
A4: now :: thesis: ( for k being Nat holds not j = k + 1 or i + 1 <= j or i + 1 = j + 1 )
given k being Nat such that A5: j = k + 1 ; :: thesis: ( i + 1 <= j or i + 1 = j + 1 )
i <= k + 1 by A3, A5, XREAL_1:6;
hence ( i + 1 <= j or i + 1 = j + 1 ) by A2, A5, XREAL_1:6; :: thesis: verum
end;
now :: thesis: ( not j = 0 or i + 1 <= j or i + 1 = j + 1 )
A6: 0 <= i by Th2;
assume A7: j = 0 ; :: thesis: ( i + 1 <= j or i + 1 = j + 1 )
then i <= 0 by A3, XREAL_1:6;
hence ( i + 1 <= j or i + 1 = j + 1 ) by A7, A6; :: thesis: verum
end;
hence ( i + 1 <= j or i + 1 = j + 1 ) by A4, Th6; :: thesis: verum
end;
A8: S1[ 0 ] by Th2;
for i being Nat holds S1[i] from NAT_1:sch 2(A8, A1);
 hence ( not i <= j + 1 or i <= j or i = j + 1 ) by A0; :: thesis: verum