let F be Function of NAT,(bool REAL); :: thesis: for G being Interval_Covering of F holds inf (Svc (union (rng F))) <= SUM (vol G)
let G be Interval_Covering of F; :: thesis: inf (Svc (union (rng F))) <= SUM (vol G)
consider H being Function of NAT,[: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 ext-real number st x in rng (Ser ((On (G,H)) vol)) holds
ex y being ext-real number st
( y in rng (Ser (vol G)) & x <= y )

proof

let x be ext-real number ; :: thesis: ( x in rng (Ser ((On (G,H)) vol)) implies ex y being ext-real number st
( y in rng (Ser (vol G)) & x <= y ) )
assume x in rng (Ser ((On (G,H)) vol)) ; :: thesis: ex y being ext-real number st
( y in rng (Ser (vol G)) & x <= y )
then consider n being set 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 Function of NAT,(bool REAL)
for G being Interval_Covering of F holds (Ser ((On (G,H)) vol)) . n <= (Ser (vol G)) . m by A1, A2, Th15;
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;

set Q = vol (On (G,H));
vol (On (G,H)) in Svc (union (rng F)) by Def8;
then A7: inf (Svc (union (rng F))) <= vol (On (G,H)) by XXREAL_2:3;
( SUM ((On (G,H)) vol) = sup (rng (Ser ((On (G,H)) vol))) & SUM (vol G) = sup (rng (Ser (vol G))) ) by SUPINF_2:def 17;
then vol (On (G,H)) <= SUM (vol G) by A3, XXREAL_2:63;
hence inf (Svc (union (rng F))) <= SUM (vol G) by A7, XXREAL_0:2; :: thesis: verum