let X be set ; :: thesis: for S being SigmaField of X
for N, F being Function of NAT ,S st F . 0 = {} & ( for n being Element of 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 Function of NAT ,S st F . 0 = {} & ( for n being Element of 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 Function of NAT ,S; :: thesis: ( F . 0 = {} & ( for n being Element of 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 Element of 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 Element of NAT holds F . n c= F . (n + 1) by Th15;
( rng F c= S & rng F is N_Sub_set_fam of X ) by MEASURE1:52, RELAT_1:def 19;
hence rng F is non-decreasing N_Measure_fam of S by A1, Def1, Def2; :: thesis: verum