theorem :: MESFUN6C:49

for X being non empty set
for S being SigmaField of X
for A being Element of S
for f being PartFunc of X,REAL
for a being Real holds A /\ (eq_dom (f,a)) = (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a))