theorem :: COUNTERS:12

for N, M being ExtNat st N <= M & M <= N + 1 & not N = M holds
M = N + 1