let M be non empty MetrSpace; :: thesis: for X being Subset of (TopSpaceMetr M)
for x being object holds
( x in Cl X iff ex S being sequence of M st
( ( for n being Nat holds S . n in X ) & S is convergent & lim S = x ) )
let X be Subset of (TopSpaceMetr M); :: thesis: for x being object holds
( x in Cl X iff ex S being sequence of M st
( ( for n being Nat holds S . n in X ) & S is convergent & lim S = x ) )
let x be object ; :: thesis: ( x in Cl X iff ex S being sequence of M st
( ( for n being Nat holds S . n in X ) & S is convergent & lim S = x ) )

hereby :: thesis: ( ex S being sequence of M st
( ( for n being Nat holds S . n in X ) & S is convergent & lim S = x ) implies x in Cl X )

assume A1: x in Cl X ; :: thesis: ex S being sequence of M st
( ( for n being Nat holds S . n in X ) & S is convergent & lim S = x )
reconsider x0 = x as Element of M by A1;
defpred S₁[ Element of NAT , object ] means ( $2 in X & $2 in Ball (x0,(1 / ($1 + 1))) );
A2: for n being Element of NAT ex p being Element of M st S₁[n,p]

proof

let n be Element of NAT ; :: thesis: ex p being Element of M st S₁[n,p]
set r = 1 / (n + 1);
reconsider G = Ball (x0,(1 / (n + 1))) as Subset of (TopSpaceMetr M) ;
dist (x0,x0) = 0 by METRIC_1:1;
then ( G is open & x0 in G ) by METRIC_1:11, TOPMETR:14;
then X meets Ball (x0,(1 / (n + 1))) by A1, PRE_TOPC:def 7;
then consider p being object such that
A3: p in X /\ (Ball (x0,(1 / (n + 1)))) by XBOOLE_0:def 1;
reconsider p = p as Element of M by A3;
take p ; :: thesis: S₁[n,p]
thus S₁[n,p] by A3, XBOOLE_0:def 4; :: thesis: verum

end;

consider S being sequence of M such that
A4: for n being Element of NAT holds S₁[n,S . n] from FUNCT_2:sch 3(A2);

A5: now :: thesis: for n being Nat holds
( S . n in X & dist ((S . n),x0) < 1 / (n + 1) )

let n be Nat; :: thesis: ( S . n in X & dist ((S . n),x0) < 1 / (n + 1) )
n in NAT by ORDINAL1:def 12;
then ( S . n in X & S . n in Ball (x0,(1 / (n + 1))) ) by A4;
hence ( S . n in X & dist ((S . n),x0) < 1 / (n + 1) ) by METRIC_1:11; :: thesis: verum

end;

A6: now :: thesis: for s being Real st 0 < s holds
ex k being Nat st
for m being Nat st k <= m holds
dist ((S . m),x0) < s

let s be Real; :: thesis: ( 0 < s implies ex k being Nat st
for m being Nat st k <= m holds
dist ((S . m),x0) < s )
assume A7: 0 < s ; :: thesis: ex k being Nat st
for m being Nat st k <= m holds
dist ((S . m),x0) < s
consider n being Nat such that
A8: s " < n by SEQ_4:3;
take k = n; :: thesis: for m being Nat st k <= m holds
dist ((S . m),x0) < s
let m be Nat; :: thesis: ( k <= m implies dist ((S . m),x0) < s )
assume k <= m ; :: thesis: dist ((S . m),x0) < s
then k + 1 <= m + 1 by XREAL_1:6;
then A9: 1 / (m + 1) <= 1 / (k + 1) by XREAL_1:118;
(s ") + 0 < n + 1 by A8, XREAL_1:8;
then 1 / (n + 1) < 1 / (s ") by A7, XREAL_1:76;
then 1 / (m + 1) < s by A9, XXREAL_0:2;
hence dist ((S . m),x0) < s by A5, XXREAL_0:2; :: thesis: verum

end;

then A10: S is convergent ;
then lim S = x by A6, TBSP_1:def 3;
hence ex S being sequence of M st
( ( for n being Nat holds S . n in X ) & S is convergent & lim S = x ) by A5, A10; :: thesis: verum

end;

given S being sequence of M such that A11: for n being Nat holds S . n in X and
A12: S is convergent and
A13: lim S = x ; :: thesis: x in Cl X
X c= Cl X by PRE_TOPC:18;
then A14: for n being Nat holds S . n in Cl X by A11, TARSKI:def 3;
Cl (Cl X) = Cl X ;
hence x in Cl X by A12, A13, A14, PRE_TOPC:22, TOPMETR3:1; :: thesis: verum