let X be RealBanachSpace; :: thesis: for Y being SetSequence of X st union (rng Y) = the carrier of X & ( for n being Element of NAT holds Y . n is closed ) holds
ex n0 being Element of NAT ex r being Real ex x0 being Point of X st
( 0 < r & Ball (x0,r) c= Y . n0 )
let Y be SetSequence of X; :: thesis: ( union (rng Y) = the carrier of X & ( for n being Element of NAT holds Y . n is closed ) implies ex n0 being Element of NAT ex r being Real ex x0 being Point of X st
( 0 < r & Ball (x0,r) c= Y . n0 ) )
assume that
A1: union (rng Y) = the carrier of X and
A2: for n being Element of NAT holds Y . n is closed ; :: thesis: ex n0 being Element of NAT ex r being Real ex x0 being Point of X st
( 0 < r & Ball (x0,r) c= Y . n0 )

now

let n be Element of NAT ; :: thesis: (Y . n) ` in Family_open_set (MetricSpaceNorm X)
reconsider Yn = Y . n as Subset of (TopSpaceNorm X) ;
Y . n is closed by A2;
then Yn is closed by NORMSP_2:15;
then Yn ` is open by TOPS_1:29;
hence (Y . n) ` in Family_open_set (MetricSpaceNorm X) by PRE_TOPC:def 5; :: thesis: verum

end;

then consider n0 being Element of NAT , r being Real, xx0 being Point of (MetricSpaceNorm X) such that
A3: ( 0 < r & Ball (xx0,r) c= Y . n0 ) by A1, NORMSP_2:1;
consider x0 being Point of X such that
x0 = xx0 and
A4: Ball (xx0,r) = { x where x is Point of X : ||.(x0 - x).|| < r } by NORMSP_2:2;
Ball (x0,r) = { x where x is Point of X : ||.(x0 - x).|| < r } ;
hence ex n0 being Element of NAT ex r being Real ex x0 being Point of X st
( 0 < r & Ball (x0,r) c= Y . n0 ) by A3, A4; :: thesis: verum