for X being non empty set
for f being PartFunc of X,REAL
for r being Real st f is nonnegative holds
( ( 0 <= r implies r (#) f is nonnegative ) & ( r <= 0 implies r (#) f is nonpositive ) )