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