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 & x in A ) and
A2: for n being Nat ex m being Nat st
( n <= m & not S . m in A ) ;
defpred S₁[ set ] means not $1 in A;
A3: for n being Element of NAT ex m being Element of NAT st
( n <= m & S₁[S . m] )

proof

let n be Element of NAT ; :: thesis: ex m being Element of NAT st
( n <= m & S₁[S . m] )
consider m being Nat such that
A4: ( n <= m & not S . m in A ) by A2;
reconsider m = m as Element of NAT by ORDINAL1:def 12;
take m ; :: thesis: ( n <= m & S₁[S . m] )
thus ( n <= m & S₁[S . m] ) by A4; :: thesis: verum

end;

consider S1 being subsequence of S such that
A5: for n being Element of NAT holds S₁[S1 . n] from VALUED_1:sch 1(A3);
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 Nat ex m being Nat st
( n <= m & not S2 . m in U1 ) ) )

proof

take A ; :: thesis: ( A is open & x in A & ( for n being Nat ex m being Nat st
( n <= m & not S2 . m in A ) ) )
consider NS being increasing sequence of NAT such that
A6: S2 = S1 * NS by VALUED_0:def 17;
thus ( A is open & x in A ) by A1; :: thesis: for n being Nat ex m being Nat st
( n <= m & not S2 . m in A )
let n be Nat; :: thesis: ex m being 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
n in NAT by ORDINAL1:def 12;
then n in dom S2 by NORMSP_1:12;
then S2 . n = S1 . (NS . n) by A6, FUNCT_1:12;
hence not S2 . n in A by A5; :: thesis: verum

end;

hence not S2 is_convergent_to x ; :: thesis: verum