A c= union (rng G0) by Lm5;
then reconsider G0 = G0 as Interval_Covering of A by Lm6, MEASURE7:def 2;
take G0 ; :: thesis: for n being Element of NAT holds G0 . n is open_interval
thus for n being Element of NAT holds G0 . n is open_interval by Lm7; :: thesis: verum