let X be non empty MetrSpace; :: thesis: for x being Element of X
for S being sequence of X st ( for V being Subset of X st x in V & V in Family_open_set X holds
V contains_almost_all_sequence S ) holds
S is_convergent_in_metrspace_to x
let x be Element of X; :: thesis: for S being sequence of X st ( for V being Subset of X st x in V & V in Family_open_set X holds
V contains_almost_all_sequence S ) holds
S is_convergent_in_metrspace_to x
let S be sequence of X; :: thesis: ( ( for V being Subset of X st x in V & V in Family_open_set X holds
V contains_almost_all_sequence S ) implies S is_convergent_in_metrspace_to x )
A1: for r being Real st 0 < r holds
x in Ball x,r

proof

let r be Real; :: thesis: ( 0 < r implies x in Ball x,r )
assume 0 < r ; :: thesis: x in Ball x,r
then dist x,x < r by METRIC_1:1;
hence x in Ball x,r by METRIC_1:12; :: thesis: verum

end;

assume A2: for V being Subset of X st x in V & V in Family_open_set X holds
V contains_almost_all_sequence S ; :: thesis: S is_convergent_in_metrspace_to x
for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
dist (S . n),x < r

proof

let r be Real; :: thesis: ( 0 < r implies ex m being Element of NAT st
for n being Element of NAT st m <= n holds
dist (S . n),x < r )
assume 0 < r ; :: thesis: ex m being Element of NAT st
for n being Element of NAT st m <= n holds
dist (S . n),x < r
then x in Ball x,r by A1;
then Ball x,r contains_almost_all_sequence S by A2, PCOMPS_1:33;
then consider m1 being Element of NAT such that
A3: for n being Element of NAT st m1 <= n holds
S . n in Ball x,r by Def12;
take k = m1; :: thesis: for n being Element of NAT st k <= n holds
dist (S . n),x < r
let n be Element of NAT ; :: thesis: ( k <= n implies dist (S . n),x < r )
assume k <= n ; :: thesis: dist (S . n),x < r
then S . n in Ball x,r by A3;
hence dist (S . n),x < r by METRIC_1:12; :: thesis: verum

end;

hence S is_convergent_in_metrspace_to x by Def8; :: thesis: verum