let T be non empty TopStruct ; :: thesis: for S being sequence of T
for x being Point of T st x is_a_cluster_point_of S holds
x in Cl (rng S)
let S be sequence of T; :: thesis: for x being Point of T st x is_a_cluster_point_of S holds
x in Cl (rng S)
let x be Point of T; :: thesis: ( x is_a_cluster_point_of S implies x in Cl (rng S) )
assume A1: x is_a_cluster_point_of S ; :: thesis: x in Cl (rng S)
for G being Subset of T st G is open & x in G holds
rng S meets G
proof
let G be Subset of T; :: thesis: ( G is open & x in G implies rng S meets G )
assume A2: G is open ; :: thesis: ( not x in G or rng S meets G )
assume x in G ; :: thesis: rng S meets G
then consider m being Element of NAT such that
0 <= m and
A3: S . m in G by A1, A2;
m in NAT ;
then m in dom S by NORMSP_1:12;
then S . m in rng S by FUNCT_1:def 3;
then S . m in (rng S) /\ G by A3, XBOOLE_0:def 4;
hence rng S meets G ; :: thesis: verum
end;
hence x in Cl (rng S) by PRE_TOPC:def 7; :: thesis: verum