theorem Th4: :: MESFUN15:2

for X, A being set
for f being PartFunc of X,REAL st f is nonpositive holds
f | A is nonpositive