let F be sequence of (bool REAL); :: thesis: for G being Open_Interval_Covering of F holds inf (Svc2 (union (rng F))) <= SUM (vol G)
let G be Open_Interval_Covering of F; :: thesis: inf (Svc2 (union (rng F))) <= SUM (vol G)
consider H being sequence of [:NAT,NAT:] such that
A1: H is one-to-one and
dom H = NAT and
A2: rng H = [:NAT,NAT:] by MEASURE6:1;
set GG = On (G,H);
A3: for x being ExtReal st x in rng (Ser ((On (G,H)) vol)) holds
ex y being ExtReal st
( y in rng (Ser (vol G)) & x <= y )

proof

let x be ExtReal; :: thesis: ( x in rng (Ser ((On (G,H)) vol)) implies ex y being ExtReal st
( y in rng (Ser (vol G)) & x <= y ) )
assume x in rng (Ser ((On (G,H)) vol)) ; :: thesis: ex y being ExtReal st
( y in rng (Ser (vol G)) & x <= y )
then consider n being object such that
A4: n in dom (Ser ((On (G,H)) vol)) and
A5: x = (Ser ((On (G,H)) vol)) . n by FUNCT_1:def 3;
reconsider n = n as Element of NAT by A4;
consider m being Element of NAT such that
A6: for F being sequence of (bool REAL)
for G being Open_Interval_Covering of F holds (Ser ((On (G,H)) vol)) . n <= (Ser (vol G)) . m by A1, A2, Th34;
take (Ser (vol G)) . m ; :: thesis: ( (Ser (vol G)) . m in rng (Ser (vol G)) & x <= (Ser (vol G)) . m )
dom (Ser (vol G)) = NAT by FUNCT_2:def 1;
hence ( (Ser (vol G)) . m in rng (Ser (vol G)) & x <= (Ser (vol G)) . m ) by A5, A6, FUNCT_1:def 3; :: thesis: verum

end;

reconsider GG = On (G,H) as Open_Interval_Covering of union (rng F) by A2, Th31;
set Q = vol GG;
vol GG in Svc2 (union (rng F)) by Def7;
then A7: inf (Svc2 (union (rng F))) <= vol GG by XXREAL_2:3;
SUM (GG vol) <= SUM (vol G) by A3, XXREAL_2:63;
then vol GG <= SUM (vol G) by MEASURE7:def 6;
hence inf (Svc2 (union (rng F))) <= SUM (vol G) by A7, XXREAL_0:2; :: thesis: verum