let T be non empty TopStruct ; :: thesis: for S being sequence of T
for x being Point of T st not S is_convergent_to x holds
ex S1 being subsequence of S st
for S2 being subsequence of S1 holds not S2 is_convergent_to x
let S be sequence of T; :: thesis: for x being Point of T st not S is_convergent_to x holds
ex S1 being subsequence of S st
for S2 being subsequence of S1 holds not S2 is_convergent_to x
let x be Point of T; :: thesis: ( not S is_convergent_to x implies ex S1 being subsequence of S st
for S2 being subsequence of S1 holds not S2 is_convergent_to x )
assume not S is_convergent_to x ; :: thesis: ex S1 being subsequence of S st
for S2 being subsequence of S1 holds not S2 is_convergent_to x
then consider A being Subset of T such that
A1: A is open and
A2: x in A and
A3: for n being Element of NAT ex m being Element of NAT st
( n <= m & not S . m in A ) by FRECHET:def 2;
defpred S₁[ set ] means not $1 in A;
A4: for n being Element of NAT ex m being Element of NAT st
( n <= m & S₁[S . m] ) by A3;
consider S1 being subsequence of S such that
A6: for n being Element of NAT holds S₁[S1 . n] from VALUED_1:sch 1(A4);
take S1 ; :: thesis: for S2 being subsequence of S1 holds not S2 is_convergent_to x
let S2 be subsequence of S1; :: thesis: not S2 is_convergent_to x
ex U1 being Subset of T st
( U1 is open & x in U1 & ( for n being Element of NAT ex m being Element of NAT st
( n <= m & not S2 . m in U1 ) ) )

proof

take A ; :: thesis: ( A is open & x in A & ( for n being Element of NAT ex m being Element of NAT st
( n <= m & not S2 . m in A ) ) )
thus ( A is open & x in A ) by A1, A2; :: thesis: for n being Element of NAT ex m being Element of NAT st
( n <= m & not S2 . m in A )
let n be Element of NAT ; :: thesis: ex m being Element of NAT st
( n <= m & not S2 . m in A )
take n ; :: thesis: ( n <= n & not S2 . n in A )
thus n <= n ; :: thesis: not S2 . n in A
consider NS being increasing sequence of NAT such that
A7: S2 = S1 * NS by VALUED_0:def 17;
n in NAT ;
then n in dom S2 by NORMSP_1:17;
then S2 . n = S1 . (NS . n) by A7, FUNCT_1:22;
hence not S2 . n in A by A6; :: thesis: verum

end;

hence not S2 is_convergent_to x by FRECHET:def 2; :: thesis: verum