let i, j be Nat; :: thesis: ( i <= j & j <= i + 1 & not i = j implies j = i + 1 )
assume A1: ( i <= j & j <= i + 1 ) ; :: thesis: ( i = j or j = i + 1 )
then ( j <= i or j = i + 1 ) by Th8;
hence ( i = j or j = i + 1 ) by A1, XXREAL_0:1; :: thesis: verum