reconsider N = NAT as Subset of REAL by NUMBERS:19;
take N ; :: thesis: ( not N is empty & N is ordinal )
thus ( not N is empty & N is ordinal ) ; :: thesis: verum