consider A being set such that
A1: A in S by PROB_1:10;
reconsider A = A as Subset of X by A1;
set B = A;
set C = A;
consider F being Function of NAT ,(bool X) such that
A2: ( rng F = {A,A} & F . 0 = A & ( for n being Element of NAT st 0 < n holds
F . n = A ) ) by MEASURE1:40;
A3: ( rng F = {A} & F . 0 = A & ( for n being Element of NAT st 0 < n holds
F . n = A ) ) by A2, ENUMSET1:69;
then rng F c= S by A1, ZFMISC_1:37;
then reconsider F = F as Function of NAT ,S by FUNCT_2:8;
A4: {A} is N_Sub_set_fam of X by A3, SUPINF_2:def 14;
{A} c= S by A1, ZFMISC_1:37;
then reconsider T = {A} as N_Measure_fam of S by A4, Def1;
take T ; :: thesis: T is non-increasing
take F ; :: according to MEASURE2:def 3 :: thesis: ( T = rng F & ( for n being Element of NAT holds F . (n + 1) c= F . n ) )
for n being Element of NAT holds F . (n + 1) c= F . n

proof

let n be Element of NAT ; :: thesis: F . (n + 1) c= F . n
( F . n = A & F . (n + 1) = A ) by A2, NAT_1:3;
hence F . (n + 1) c= F . n ; :: thesis: verum

end;

hence ( T = rng F & ( for n being Element of NAT holds F . (n + 1) c= F . n ) ) by A2, ENUMSET1:69; :: thesis: verum