let A be Subset of REAL; :: thesis: G0 is Open_Interval_Covering of A
A c= union (rng G0) by Lm5;
then reconsider G0 = G0 as Interval_Covering of A by Lm6, MEASURE7:def 2;
for n being Element of NAT holds G0 . n is open_interval by Lm7;
hence G0 is Open_Interval_Covering of A by Def5; :: thesis: verum