REAL c= REAL ;
then consider F0 being Function of NAT ,(bool REAL ) such that
A1: rng F0 = {REAL ,({} REAL )} and
A2: ( F0 . 0 = REAL & ( for n being Element of NAT st 0 < n holds
F0 . n = {} REAL ) ) by MEASURE1:40;
( union {REAL ,{} } = REAL \/ {} & ( for n being Element of NAT holds F0 . n is Interval ) ) by A2, NAT_1:3, ZFMISC_1:93;
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 XBOOLE_0:sch 1();
vol F0 in D by A3;
hence not Svc A is empty by Def8; :: thesis: verum