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