consider A being set such that

A1: A in S by PROB_1:4;

reconsider A = A as Subset of X by A1;

consider B, C being Subset of X such that

A2: ( B = A & C = A ) ;

A3: {A} c= S by A1, ZFMISC_1:31;

consider F being sequence of (bool X) such that

A4: rng F = {B,C} and

A5: ( F . 0 = B & ( for n being Nat st 0 < n holds

F . n = C ) ) by MEASURE1:19;

A6: rng F = {A} by A2, A4, ENUMSET1:29;

then A7: rng F c= S by A1, ZFMISC_1:31;

{A} is N_Sub_set_fam of X by A6, SUPINF_2:def 8;

then reconsider T = {A} as N_Measure_fam of S by A3, Def1;

reconsider F = F as sequence of S by A7, FUNCT_2:6;

take T ; :: thesis: T is non-decreasing

take F ; :: according to MEASURE2:def 2 :: thesis: ( T = rng F & ( for n being Nat holds F . n c= F . (n + 1) ) )

for n being Nat holds F . n c= F . (n + 1)

A1: A in S by PROB_1:4;

reconsider A = A as Subset of X by A1;

consider B, C being Subset of X such that

A2: ( B = A & C = A ) ;

A3: {A} c= S by A1, ZFMISC_1:31;

consider F being sequence of (bool X) such that

A4: rng F = {B,C} and

A5: ( F . 0 = B & ( for n being Nat st 0 < n holds

F . n = C ) ) by MEASURE1:19;

A6: rng F = {A} by A2, A4, ENUMSET1:29;

then A7: rng F c= S by A1, ZFMISC_1:31;

{A} is N_Sub_set_fam of X by A6, SUPINF_2:def 8;

then reconsider T = {A} as N_Measure_fam of S by A3, Def1;

reconsider F = F as sequence of S by A7, FUNCT_2:6;

take T ; :: thesis: T is non-decreasing

take F ; :: according to MEASURE2:def 2 :: thesis: ( T = rng F & ( for n being Nat holds F . n c= F . (n + 1) ) )

for n being Nat holds F . n c= F . (n + 1)

proof

hence
( T = rng F & ( for n being Nat holds F . n c= F . (n + 1) ) )
by A2, A4, ENUMSET1:29; :: thesis: verum
let n be Nat; :: thesis: F . n c= F . (n + 1)

F . n = A by A2, A5, NAT_1:3;

hence F . n c= F . (n + 1) by A2, A5, NAT_1:3; :: thesis: verum

end;F . n = A by A2, A5, NAT_1:3;

hence F . n c= F . (n + 1) by A2, A5, NAT_1:3; :: thesis: verum