reconsider N = NAT as V85() Subset of ExtREAL by Def8, Th33;
take N ; :: thesis: N is nonnegative
thus for x being ExtReal st x in N holds
0. <= x ; :: according to SUPINF_2:def 9 :: thesis: verum