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 5;
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 5; :: 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 23;
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