theorem Th17: :: MEASURE3:17

for X being set
for S being SigmaField of X
for M being sigma_Measure of S
for F being sequence of (bool X) st ( for n being Element of NAT holds F . n is thin of M ) holds
ex G being sequence of S st
for n being Element of NAT holds
( F . n c= G . n & M . (G . n) = 0. )