:: deftheorem Def6 defines Open_Interval_Covering MEASUR12:def 6 :
for F being sequence of (bool REAL)
for b₂ being Interval_Covering of F holds
( b₂ is Open_Interval_Covering of F iff for n being Element of NAT holds b₂ . n is Open_Interval_Covering of F . n );