let F be sequence of (bool REAL); for G being Interval_Covering of F holds inf (Svc (union (rng F))) <= SUM (vol G)
let G be Interval_Covering of F; inf (Svc (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 )
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;
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; verum