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 )

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

hence
meet T is measure_zero of M
by MEASURE1:36, SETFAM_1:3; :: thesis: verum
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 A1, A2, FUNCT_2:4; :: thesis: verum

end;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 A1, A2, FUNCT_2:4; :: thesis: verum