( 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

then reconsider CA = CA as Covering of A,F by A1, Def3;

defpred S_{1}[ 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 & S_{1}[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

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

then
( union {X,{}} = X \/ {} & CA is Set_Sequence of F )
by Def2, ZFMISC_1:75;
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;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

then reconsider CA = CA as Covering of A,F by A1, Def3;

defpred S

consider D being set such that

A3: for x being object holds

( x in D iff ( x in ExtREAL & S

SUM (vol (M,CA)) in D by A3;

hence not Svc (M,A) is empty by Def7; :: thesis: verum