theorem Th1: :: MESFUN11:1

for X being non empty set
for f being nonpositive PartFunc of X,ExtREAL
for E being set holds f | E is nonpositive