REAL c= REAL ;
then consider F0 being sequence of (bool REAL) such that
A1: rng F0 = {REAL,({} REAL)} and
A2: ( F0 . 0 = REAL & ( for n being Nat st 0 < n holds
F0 . n = {} REAL ) ) by MEASURE1:19;
( union {REAL,{}} = REAL \/ {} & ( for n being Element of NAT holds F0 . n is Interval ) ) by A2, NAT_1:3, ZFMISC_1:75;
then reconsider F0 = F0 as Interval_Covering of A by A1, Def2;
defpred S₁[ set ] means ex F being Interval_Covering of A st A = vol F;
consider D being set such that
A3: for x being set holds
( x in D iff ( x in ExtREAL & S₁[x] ) ) from XFAMILY:sch 1();
vol F0 in D by A3;
hence not Svc A is empty by Def8; :: thesis: verum