let T be non empty TopStruct ; :: thesis: for S being sequence of T
for x being Point of T st ex S1 being subsequence of S st S1 is_convergent_to x holds
x is_a_cluster_point_of S
let S be sequence of T; :: thesis: for x being Point of T st ex S1 being subsequence of S st S1 is_convergent_to x holds
x is_a_cluster_point_of S
let x be Point of T; :: thesis: ( ex S1 being subsequence of S st S1 is_convergent_to x implies x is_a_cluster_point_of S )
given S1 being subsequence of S such that A1: S1 is_convergent_to x ; :: thesis: x is_a_cluster_point_of S
let O be Subset of T; :: according to FRECHET2:def 3 :: thesis: for n being Nat st O is open & x in O holds
ex m being Element of NAT st
( n <= m & S . m in O )
let n be Nat; :: thesis: ( O is open & x in O implies ex m being Element of NAT st
( n <= m & S . m in O ) )
assume ( O is open & x in O ) ; :: thesis: ex m being Element of NAT st
( n <= m & S . m in O )
then consider n1 being Nat such that
A2: for m being Nat st n1 <= m holds
S1 . m in O by A1;
reconsider n2 = max (n1,n) as Element of NAT by ORDINAL1:def 12;
A3: S1 . n2 in O by A2, XXREAL_0:25;
consider NS being increasing sequence of NAT such that
A4: S1 = S * NS by VALUED_0:def 17;
take NS . n2 ; :: thesis: ( n <= NS . n2 & S . (NS . n2) in O )
( n <= n2 & n2 <= NS . n2 ) by SEQM_3:14, XXREAL_0:25;
hence n <= NS . n2 by XXREAL_0:2; :: thesis: S . (NS . n2) in O
n2 in NAT ;
then n2 in dom NS by FUNCT_2:def 1;
hence S . (NS . n2) in O by A4, A3, FUNCT_1:13; :: thesis: verum