:: deftheorem Def5 defines Open_Interval_Covering MEASUR12:def 5 :
for A being Subset of REAL
for b₂ being Interval_Covering of A holds
( b₂ is Open_Interval_Covering of A iff for n being Element of NAT holds b₂ . n is open_interval );