let i, j be natural Number ; :: thesis: ( i <= j & j <= i + 1 & not i = j implies j = i + 1 )
assume that
A1: i <= j and
A2: j <= i + 1 ; :: thesis: ( i = j or j = i + 1 )
( j <= i or j = i + 1 ) by A2, Th8;
hence ( i = j or j = i + 1 ) by A1, XXREAL_0:1; :: thesis: verum