let T be non empty TopStruct ; :: thesis: for A being Subset of T
for S being sequence of T
for x being Point of T st rng S c= A & x in Lim S holds
x in Cl A
let A be Subset of T; :: thesis: for S being sequence of T
for x being Point of T st rng S c= A & x in Lim S holds
x in Cl A
let S be sequence of T; :: thesis: for x being Point of T st rng S c= A & x in Lim S holds
x in Cl A
let x be Point of T; :: thesis: ( rng S c= A & x in Lim S implies x in Cl A )
assume that
A1: rng S c= A and
A2: x in Lim S ; :: thesis: x in Cl A
for O being Subset of T st O is open & x in O holds
A meets O
proof
let O be Subset of T; :: thesis: ( O is open & x in O implies A meets O )
assume A3: O is open ; :: thesis: ( not x in O or A meets O )
A4: S is_convergent_to x by A2, FRECHET:def 5;
assume x in O ; :: thesis: A meets O
then consider n being Nat such that
A5: for m being Nat st n <= m holds
S . m in O by A3, A4;
n in NAT by ORDINAL1:def 12;
then n in dom S by NORMSP_1:12;
then A6: S . n in rng S by FUNCT_1:def 3;
S . n in O by A5;
then S . n in A /\ O by A1, A6, XBOOLE_0:def 4;
hence A meets O ; :: thesis: verum
end;
hence x in Cl A by PRE_TOPC:def 7; :: thesis: verum