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 & dom H = NAT & rng H = [:NAT ,NAT :] ) by MEASURE6:1;
set GG = On G,H;
set Q = vol (On G,H);
A2: SUM ((On G,H) vol ) = sup (rng (Ser ((On G,H) vol ))) by SUPINF_2:def 23;
A3: SUM (vol G) = sup (rng (Ser (vol G))) by SUPINF_2:def 23;
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 )) & 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
A5: 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, 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 & m in NAT ) by FUNCT_2:def 1;
hence ( (Ser (vol G)) . m in rng (Ser (vol G)) & x <= (Ser (vol G)) . m ) by A4, A5, FUNCT_1:def 5; :: thesis: verum

end;

then A6: vol (On G,H) <= SUM (vol G) by A2, A3, XXREAL_2:63;
vol (On G,H) in Svc (union (rng F)) by Def8;
then inf (Svc (union (rng F))) <= vol (On G,H) by XXREAL_2:3;
hence inf (Svc (union (rng F))) <= SUM (vol G) by A6, XXREAL_0:2; :: thesis: verum