reconsider N = NAT as Denum_Set_of_R_EAL by Def14, Th52;
take N ; :: thesis: N is nonnegative
thus for x being R_eal st x in N holds
0. <= x by NAT_1:2; :: according to SUPINF_2:def 9 :: thesis: verum