:: deftheorem Def3 defines Covering MEASURE8:def 3 :
for X being set
for A being Subset of X
for F being Field_Subset of X
for b₄ being Set_Sequence of F holds
( b₄ is Covering of A,F iff A c= union (rng b₄) );