( X c= X & {} c= X ) ;
then consider CA being sequence of (bool X) such that
A1: rng CA = {X,{}} and
CA . 0 = X and
for n being Nat st 0 < n holds
CA . n = {} by MEASURE1:19;
for n being Nat holds CA . n in F
proof
let n be Nat; :: thesis: CA . n in F
n in NAT by ORDINAL1:def 12;
then A2: CA . n in rng CA by FUNCT_2:4;
( X in F & {} in F ) by PROB_1:4, PROB_1:5;
then rng CA c= F by A1, ZFMISC_1:32;
hence CA . n in F by A2; :: thesis: verum
end;
then ( union {X,{}} = X \/ {} & CA is Set_Sequence of F ) by Def2, ZFMISC_1:75;
then reconsider CA = CA as Covering of A,F by A1, Def3;
defpred S1[ object ] means ex G being Covering of A,F st X = SUM (vol (M,G));
consider D being set such that
A3: for x being object holds
( x in D iff ( x in ExtREAL & S1[x] ) ) from XBOOLE_0:sch 1();
 SUM (vol (M,CA)) in D by A3;
hence not Svc (M,A) is empty by Def7; :: thesis: verum