:: deftheorem defines nonpositive MESFUNC5:def 1 :
for IT being set holds
( IT is nonpositive iff for x being R_eal st x in IT holds
x <= 0 );