theorem Th13: :: MESFUNC6:13

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