theorem Th3: :: LOPBAN_5:3

for X being RealBanachSpace
for Y being SetSequence of X st union (rng Y) = the carrier of X & ( for n being Nat holds Y . n is closed ) holds
ex n0 being Nat ex r being Real ex x0 being Point of X st
( 0 < r & Ball (x0,r) c= Y . n0 )