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

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