:: deftheorem Def4 defines Covering MEASURE8:def 4 :
for X being set
for F being Field_Subset of X
for Sets being SetSequence of X
for b₄ being sequence of (Funcs (NAT,(bool X))) holds
( b₄ is Covering of Sets,F iff for n being Nat holds b₄ . n is Covering of Sets . n,F );