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, MEASURE7:def 2;
for n being Element of NAT holds F0 . n is open_interval

proof

let n be Element of NAT ; :: thesis: F0 . n is open_interval

per cases ( n = 0 or n <> 0 ) ;

suppose n = 0 ; :: thesis: F0 . n is open_interval

hence F0 . n is open_interval by A2, Lm7; :: thesis: verum

end;

suppose n <> 0 ; :: thesis: F0 . n is open_interval

hence F0 . n is open_interval by A2; :: thesis: verum

end;

end;

end;

then reconsider F0 = F0 as Open_Interval_Covering of A by Def5;
defpred S₁[ set ] means ex F being Open_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();
D c= ExtREAL by A3;
then reconsider D = D as Subset of ExtREAL ;
vol F0 in D by A3;
then reconsider D = D as non empty Subset of ExtREAL ;
for x being R_eal holds
( x in D iff ex F being Open_Interval_Covering of A st x = vol F ) by A3;
hence not Svc2 A is empty by Def7; :: thesis: verum