let X be set ; :: thesis: for S being SigmaField of X

for T being N_Measure_fam of S holds

( meet T in S & union T in S )

let S be SigmaField of X; :: thesis: for T being N_Measure_fam of S holds

( meet T in S & union T in S )

let T be N_Measure_fam of S; :: thesis: ( meet T in S & union T in S )

T c= S by Def1;

hence ( meet T in S & union T in S ) by MEASURE1:22, MEASURE1:def 5; :: thesis: verum

for T being N_Measure_fam of S holds

( meet T in S & union T in S )

let S be SigmaField of X; :: thesis: for T being N_Measure_fam of S holds

( meet T in S & union T in S )

let T be N_Measure_fam of S; :: thesis: ( meet T in S & union T in S )

T c= S by Def1;

hence ( meet T in S & union T in S ) by MEASURE1:22, MEASURE1:def 5; :: thesis: verum