:: deftheorem Def2 defines Interval_Covering MEASURE7:def 2 :
for A being Subset of REAL
for b₂ being sequence of (bool REAL) holds
( b₂ is Interval_Covering of A iff ( A c= union (rng b₂) & ( for n being Element of NAT holds b₂ . n is Interval ) ) );