let X be non empty MetrSpace; :: thesis: for x being Element of X
for S being sequence of X holds
( S is_convergent_in_metrspace_to x iff 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 holds
( S is_convergent_in_metrspace_to x iff 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: ( S is_convergent_in_metrspace_to x iff for V being Subset of X st x in V & V in Family_open_set X holds
V contains_almost_all_sequence S )
thus ( S is_convergent_in_metrspace_to x implies for V being Subset of X st x in V & V in Family_open_set X holds
V 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 ) implies S is_convergent_in_metrspace_to x )

proof

assume S is_convergent_in_metrspace_to 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
then for r being Real st 0 < r holds
Ball (x,r) contains_almost_all_sequence S by Th15;
hence for V being Subset of X st x in V & V in Family_open_set X holds
V contains_almost_all_sequence S by Th16; :: thesis: verum

end;

thus ( ( 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 ) by Th17; :: thesis: verum