theorem :: MESFUN11:8

for X being non empty set
for f being PartFunc of X,ExtREAL
for r being non positive Real holds less_dom (f,r) = great_dom ((max- f),(- r)) by Lm1;