let A be Subset of REAL; :: thesis: ( Svc2 A c= Svc A & inf (Svc A) <= inf (Svc2 A) )
now :: thesis: for x being R_eal st x in Svc2 A holds
x in Svc A
let x be R_eal; :: thesis: ( x in Svc2 A implies x in Svc A )
assume x in Svc2 A ; :: thesis: x in Svc A
then ex F being Open_Interval_Covering of A st x = vol F by Def7;
hence x in Svc A by MEASURE7:def 8; :: thesis: verum
end;
hence Svc2 A c= Svc A ; :: thesis: inf (Svc A) <= inf (Svc2 A)
hence inf (Svc A) <= inf (Svc2 A) by XXREAL_2:60; :: thesis: verum