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
; T is non-decreasing
take
F
; MEASURE2:def 2 ( 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)
hence
( T = rng F & ( for n being Nat holds F . n c= F . (n + 1) ) )
by A2, A4, ENUMSET1:29; verum