theorem :: MESFUNC6:19

for X being non empty set
for S being SigmaField of X
for f, g being PartFunc of X,REAL
for A being Element of S
for r being Real st f is A -measurable & g is A -measurable & A c= dom g holds
(A /\ (less_dom (f,r))) /\ (great_dom (g,r)) in S by MESFUNC1:36;