theorem :: COUNTERS:7

for N, M being ExtNat st N < M holds
N in NAT