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