let M be non empty MetrSpace; :: thesis:
let X be Subset of (TopSpaceMetr M); :: thesis:
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:
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:
for x being object st x in Cl X holds
x in X

let x be object ; :: thesis:
assume x in Cl X ; :: thesis:
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:

end;