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 S₁[ 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 S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A2: 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 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: S₁[ 0 ] by Th2;
for i being Nat holds S₁[i] from NAT_1:sch 2(A8, A1);
hence ( not i <= j + 1 or i <= j or i = j + 1 ) by A0; :: thesis: verum