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 Element of 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 Element of 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 Element of NAT such that
A2: for m being Element of NAT st n1 <= m holds
S1 . m in O by A1, FRECHET:def 3;
set n2 = max (n1,n);
A3: S1 . (max (n1,n)) 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 . (max (n1,n)) ; :: thesis: ( n <= NS . (max (n1,n)) & S . (NS . (max (n1,n))) in O )
( n <= max (n1,n) & max (n1,n) <= NS . (max (n1,n)) ) by SEQM_3:14, XXREAL_0:25;
hence n <= NS . (max (n1,n)) by XXREAL_0:2; :: thesis: S . (NS . (max (n1,n))) in O
max (n1,n) in NAT ;
then max (n1,n) in dom NS by FUNCT_2:def 1;
hence S . (NS . (max (n1,n))) in O by A4, A3, FUNCT_1:13; :: thesis: verum