let i, j be natural Number ; :: 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

A2: now :: thesis: not i = j + 1

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

end;

i <= j + 1 by A1, Th12;
hence i < j + 1 by A2, XXREAL_0:1; :: thesis: verum