theorem :: MESFUNC1:18

for X being set
for f being PartFunc of X,ExtREAL
for A being set
for a being ExtReal holds A /\ (eq_dom (f,a)) = (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a))