let T be non empty TopStruct ; :: thesis: for S being sequence of T
for x, y being Point of T st ( for n being Element of NAT holds
( S . n = y & S is_convergent_to x ) ) holds
x in Cl {y}
let S be sequence of T; :: thesis: for x, y being Point of T st ( for n being Element of NAT holds
( S . n = y & S is_convergent_to x ) ) holds
x in Cl {y}
let x, y be Point of T; :: thesis: ( ( for n being Element of NAT holds
( S . n = y & S is_convergent_to x ) ) implies x in Cl {y} )
assume A1: for n being Element of NAT holds
( S . n = y & S is_convergent_to x ) ; :: thesis: x in Cl {y}
for G being Subset of T st G is open & x in G holds
{y} meets G
proof
let G be Subset of T; :: thesis: ( G is open & x in G implies {y} meets G )
assume A2: G is open ; :: thesis: ( not x in G or {y} meets G )
assume x in G ; :: thesis: {y} meets G
then consider n being Nat such that
A3: for m being Nat st n <= m holds
S . m in G by A1, A2, FRECHET:def 3;
A4: n in NAT by ORDINAL1:def 12;
S . n in G by A3;
then A5: y in G by A1, A4;
y in {y} by TARSKI:def 1;
then y in {y} /\ G by A5, XBOOLE_0:def 4;
hence {y} meets G ; :: thesis: verum
end;
hence x in Cl {y} by PRE_TOPC:def 7; :: thesis: verum