theorem Th13: :: MESFUNC2:13

for C being non empty set
for f being PartFunc of C,ExtREAL
for x being Element of C holds 0. <= (max- f) . x