let i, j be Nat; :: thesis: ( i < j + 1 iff i <= j )
thus ( i < j + 1 implies i <= j ) by Th8; :: thesis: ( i <= j implies i < j + 1 )
assume A1: i <= j ; :: thesis: i < j + 1
then X: i <= j + 1 by Th12;

now

assume A2: i = j + 1 ; :: thesis: contradiction
A3: j + (- j) = 0 ;
(j + 1) + (- j) = 1 ;
hence contradiction by A1, A2, A3, XREAL_1:8; :: thesis: verum

end;

hence i < j + 1 by X, XXREAL_0:1; :: thesis: verum