theorem Th31: :: MEASUR12:31

for F being sequence of (bool REAL)
for G being Open_Interval_Covering of F
for H being sequence of [:NAT,NAT:] st rng H = [:NAT,NAT:] holds
On (G,H) is Open_Interval_Covering of union (rng F)