let M be non empty MetrSpace; :: thesis: for X being Subset of (TopSpaceMetr M) holds
( X is closed iff for S being sequence of M st ( for n being Nat holds S . n in X ) & S is convergent holds
lim S in X )
let X be Subset of (TopSpaceMetr M); :: thesis: ( X is closed iff for S being sequence of M st ( for n being Nat holds S . n in X ) & S is convergent holds
lim S in X )
thus ( X is closed implies for S being sequence of M st ( for n being Nat holds S . n in X ) & S is convergent holds
lim S in X ) by TOPMETR3:1; :: thesis: ( ( for S being sequence of M st ( for n being Nat holds S . n in X ) & S is convergent holds
lim S in X ) implies X is closed )
assume A1: for S being sequence of M st ( for n being Nat holds S . n in X ) & S is convergent holds
lim S in X ; :: thesis: X is closed
for x being object st x in Cl X holds
x in X

proof

let x be object ; :: thesis: ( x in Cl X implies x in X )
assume x in Cl X ; :: thesis: x in X
then consider S being sequence of M such that
A2: ( ( for n being Nat holds S . n in X ) & S is convergent & lim S = x ) by Th3;
thus x in X by A1, A2; :: thesis: verum

end;

then Cl X = X by PRE_TOPC:18, TARSKI:def 3;
hence X is closed by PRE_TOPC:22; :: thesis: verum