theorem Th32: :: MEASUR12:32

for A being Subset of REAL
for G being sequence of (bool REAL) st A c= union (rng G) & ( for n being Element of NAT holds G . n is open_interval ) holds
G is Open_Interval_Covering of A