theorem Th34: :: MESFUN15:32
for a, b being Real
for f being PartFunc of REAL,REAL st ].a,b.] c= dom f & f is_left_improper_integrable_on a,b holds
for E being Element of L-Field st E c= ].a,b.] holds
f is E -measurable