:: deftheorem Def2 defines nonnegative MEASURE1:def 2 :
for X being non empty set
for F being Function of X,ExtREAL holds
( F is nonnegative iff for A being Element of X holds 0. <= F . A );