theorem :: MESFUN11:6

for X being non empty set
for f being PartFunc of X,ExtREAL
for x being object holds
( f . x <= (max+ f) . x & f . x >= - ((max- f) . x) )