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

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