theorem Th20: :: MESFUNC1:20

for X being set
for f being PartFunc of X,ExtREAL
for S being SigmaField of X
for F being sequence of S
for A being set
for r being Real st ( for n being Element of NAT holds F . n = A /\ (less_dom (f,(r + (1 / (n + 1))))) ) holds
A /\ (less_eq_dom (f,r)) = meet (rng F)