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 4 :: 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 that
A2: O is open and
A3: x in O ; :: thesis: ex m being Element of NAT st
( n <= m & S . m in O )
consider n1 being Element of NAT such that
A4: for m being Element of NAT st n1 <= m holds
S1 . m in O by A1, A2, A3, FRECHET:def 2;
set n2 = max n1,n;
consider NS being increasing sequence of NAT such that
A5: 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 )
A6: n <= max n1,n by XXREAL_0:25;
max n1,n <= NS . (max n1,n) by SEQM_3:33;
hence n <= NS . (max n1,n) by A6, XXREAL_0:2; :: thesis: S . (NS . (max n1,n)) in O
A7: S1 . (max n1,n) in O by A4, XXREAL_0:25;
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 A5, A7, FUNCT_1:23; :: thesis: verum