:: deftheorem Def3 defines Interval_Covering MEASURE7:def 3 :
for F being sequence of (bool REAL)
for b₂ being sequence of (Funcs (NAT,(bool REAL))) holds
( b₂ is Interval_Covering of F iff for n being Element of NAT holds b₂ . n is Interval_Covering of F . n );