for X being non empty MetrSpace
for Y being SetSequence of X st X is complete & union (rng Y) = the carrier of X & ( for n being Nat holds (Y . n) ` in Family_open_set X ) holds
ex n0 being Nat ex r being Real ex x0 being Point of X st
( 0 < r & Ball (x0,r) c= Y . n0 )