let X be non empty MetrSpace; :: thesis: for x being Element of X
for S being sequence of X st ( for r being Real st 0 < r holds
Ball (x,r) contains_almost_all_sequence S ) holds
for V being Subset of X st x in V & V in Family_open_set X holds
V contains_almost_all_sequence S
let x be Element of X; :: thesis: for S being sequence of X st ( for r being Real st 0 < r holds
Ball (x,r) contains_almost_all_sequence S ) holds
for V being Subset of X st x in V & V in Family_open_set X holds
V contains_almost_all_sequence S
let S be sequence of X; :: thesis: ( ( for r being Real st 0 < r holds
Ball (x,r) contains_almost_all_sequence S ) implies for V being Subset of X st x in V & V in Family_open_set X holds
V contains_almost_all_sequence S )
assume A1: for r being Real st 0 < r holds
Ball (x,r) contains_almost_all_sequence S ; :: thesis: for V being Subset of X st x in V & V in Family_open_set X holds
V contains_almost_all_sequence S
A2: for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
S . n in Ball (x,r) by A1, Def5;
thus for V being Subset of X st x in V & V in Family_open_set X holds
V contains_almost_all_sequence S :: thesis: verum

proof

let V be Subset of X; :: thesis: ( x in V & V in Family_open_set X implies V contains_almost_all_sequence S )
assume ( x in V & V in Family_open_set X ) ; :: thesis: V contains_almost_all_sequence S
then consider q being Real such that
A3: 0 < q and
A4: Ball (x,q) c= V by PCOMPS_1:def 4;
consider m1 being Nat such that
A5: for n being Nat st m1 <= n holds
S . n in Ball (x,q) by A2, A3;
for n being Nat st m1 <= n holds
S . n in V by A4, A5;
hence V contains_almost_all_sequence S ; :: thesis: verum

end;