( X c= X & {} c= X ) by XBOOLE_1:2;
then consider CA being Function of NAT,(bool X) such that
A1: rng CA = {X,{}} and
CA . 0 = X and
for n being Element of NAT st 0 < n holds
CA . n = {} by MEASURE1:40;
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 13;
then A2: CA . n in rng CA by FUNCT_2:6;
( X in F & {} in F ) by PROB_1:10, PROB_1:11;
then rng CA c= F by A1, ZFMISC_1:38;
hence CA . n in F by A2; :: thesis: verum

end;

then ( union {X,{}} = X \/ {} & CA is Set_Sequence of F ) by Def2, ZFMISC_1:93;
then reconsider CA = CA as Covering of A,F by A1, Def3;
defpred S₁[ set ] means ex G being Covering of A,F st X = SUM (vol (M,G));
consider D being set such that
A3: for x being set holds
( x in D iff ( x in ExtREAL & S₁[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