let X be set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for T being N_Measure_fam of S st ( for A being set st A in T holds
A is measure_zero of M ) holds
meet T is measure_zero of M

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for T being N_Measure_fam of S st ( for A being set st A in T holds
A is measure_zero of M ) holds
meet T is measure_zero of M

let M be sigma_Measure of S; :: thesis: for T being N_Measure_fam of S st ( for A being set st A in T holds
A is measure_zero of M ) holds
meet T is measure_zero of M

let T be N_Measure_fam of S; :: thesis: ( ( for A being set st A in T holds
A is measure_zero of M ) implies meet T is measure_zero of M )

assume A1: for A being set st A in T holds
A is measure_zero of M ; :: thesis: meet T is measure_zero of M
ex A being set st
( A in T & A is measure_zero of M )
proof
consider F being sequence of (bool X) such that
A2: T = rng F by SUPINF_2:def 8;
take F . 0 ; :: thesis: ( F . 0 in T & F . 0 is measure_zero of M )
thus ( F . 0 in T & F . 0 is measure_zero of M ) by ; :: thesis: verum
end;
hence meet T is measure_zero of M by ; :: thesis: verum