theorem :: MESFUNC6:53

for X being set
for f being PartFunc of X,REAL holds
( f is nonpositive iff for x being set holds f . x <= 0 )