let N, M be ExtNat; :: thesis: ( N <= M & M <= N + 1 & not N = M implies M = N + 1 )
assume A1: ( N <= M & M <= N + 1 ) ; :: thesis: ( N = M or M = N + 1 )
then ( M <= N or M = N + 1 ) by Th10;
hence ( N = M or M = N + 1 ) by A1, XXREAL_0:1; :: thesis: verum