theorem :: MESFUNC2:16

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