:: deftheorem defines nonnegative SUPINF_2:def 9 :
for IT being set holds
( IT is nonnegative iff for x being ExtReal st x in IT holds
0. <= x );