for X being set
for F being Field_Subset of X
for A being Subset of X
for CA being Covering of A,F st A in F holds
ex FSets being Sep_Sequence of F st
( A = union (rng FSets) & ( for n being Nat holds FSets . n c= CA . n ) )