theorem Th33: :: MESFUNC5:33

for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,ExtREAL
for A being Element of S
for r, s being Real st f is A -measurable & A c= dom f holds
(A /\ (great_eq_dom (f,r))) /\ (less_dom (f,s)) in S