theorem Th58: :: MESFUNC6:58

for X being non empty set
for f, g being PartFunc of X,REAL st ( for x being set st x in (dom f) /\ (dom g) holds
g . x <= f . x ) holds
f - g is nonnegative