consider A being set such that
A1: A in S by PROB_1:4;
reconsider A = A as Subset of X by A1;
A2: {A} c= S by A1, ZFMISC_1:31;
set B = A;
set C = A;
consider F being sequence of (bool X) such that
A3: rng F = {A,A} and
A4: ( F . 0 = A & ( for n being Nat st 0 < n holds
F . n = A ) ) by MEASURE1:19;
A5: rng F = {A} by A3, ENUMSET1:29;
then A6: rng F c= S by A1, ZFMISC_1:31;
{A} is N_Sub_set_fam of X by A5, SUPINF_2:def 8;
then reconsider T = {A} as N_Measure_fam of S by A2, Def1;
reconsider F = F as sequence of S by A6, FUNCT_2:6;
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 by A4, NAT_1:3;
hence F . (n + 1) c= F . n by A4, NAT_1:3; :: thesis: verum
end;
hence ( T = rng F & ( for n being Element of NAT holds F . (n + 1) c= F . n ) ) by A3, ENUMSET1:29; :: thesis: verum