theorem Th5: :: COUNTERS:6

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