:: deftheorem defines -measurable MESFUNC1:def 15 :
for X being non empty set
for S being SigmaField of X
for A being Element of S
for f being PartFunc of X,ExtREAL holds
( f is A -measurable iff for r being Real holds A /\ (less_dom (f,r)) in S );