let X be non empty MetrSpace; :: thesis: for S being sequence of X
for F being Subset of () st S is convergent & ( for n being Nat holds S . n in F ) & F is closed holds
lim S in F

let S be sequence of X; :: thesis: for F being Subset of () st S is convergent & ( for n being Nat holds S . n in F ) & F is closed holds
lim S in F

let F be Subset of (); :: thesis: ( S is convergent & ( for n being Nat holds S . n in F ) & F is closed implies lim S in F )
assume that
A1: S is convergent and
A2: for n being Nat holds S . n in F and
A3: F is closed ; :: thesis: lim S in F
A4: for G being Subset of () st G is open & lim S in G holds
F meets G
proof
let G be Subset of (); :: thesis: ( G is open & lim S in G implies F meets G )
assume A5: G is open ; :: thesis: ( not lim S in G or F meets G )
now :: thesis: ( lim S in G implies F meets G )
assume lim S in G ; :: thesis: F meets G
then consider r1 being Real such that
A6: r1 > 0 and
A7: Ball ((lim S),r1) c= G by ;
reconsider r2 = r1 as Real ;
consider n being Nat such that
A8: for m being Nat st m >= n holds
dist ((S . m),(lim S)) < r2 by ;
dist ((S . n),(lim S)) < r2 by A8;
then A9: S . n in Ball ((lim S),r1) by METRIC_1:11;
S . n in F by A2;
then S . n in F /\ G by ;
hence F meets G by XBOOLE_0:def 7; :: thesis: verum
end;
hence ( not lim S in G or F meets G ) ; :: thesis: verum
end;
reconsider F0 = F as Subset of () ;
lim S in the carrier of X ;
then lim S in the carrier of () by TOPMETR:12;
then lim S in Cl F0 by ;
hence lim S in F by ; :: thesis: verum