let X be set ; :: thesis: for S being SigmaField of X
for N, F being sequence of S st F . 0 = {} & ( for n being Nat holds
( F . (n + 1) = (N . 0) \ (N . n) & N . (n + 1) c= N . n ) ) holds
rng F is non-decreasing N_Measure_fam of S
let S be SigmaField of X; :: thesis: for N, F being sequence of S st F . 0 = {} & ( for n being Nat holds
( F . (n + 1) = (N . 0) \ (N . n) & N . (n + 1) c= N . n ) ) holds
rng F is non-decreasing N_Measure_fam of S
let N, F be sequence of S; :: thesis: ( F . 0 = {} & ( for n being Nat holds
( F . (n + 1) = (N . 0) \ (N . n) & N . (n + 1) c= N . n ) ) implies rng F is non-decreasing N_Measure_fam of S )
assume ( F . 0 = {} & ( for n being Nat holds
( F . (n + 1) = (N . 0) \ (N . n) & N . (n + 1) c= N . n ) ) ) ; :: thesis: rng F is non-decreasing N_Measure_fam of S
then A1: for n being Nat holds F . n c= F . (n + 1) by Th13;
( rng F c= S & rng F is N_Sub_set_fam of X ) by MEASURE1:23, RELAT_1:def 19;
hence rng F is non-decreasing N_Measure_fam of S by A1, Def1, Def2; :: thesis: verum