let T be non empty TopStruct ; :: thesis:
let x be Point of T; :: thesis:
let Y be Subset of T; :: thesis:
let S be sequence of T; :: thesis:
assume that
A1: Y = { y where y is Point of T : x in Cl {y} } and
A2: (rng S) /\ Y = {} and
A3: S is_convergent_to x ; :: according to XBOOLE_0:def 7 :: thesis:
defpred S₁[ Nat, set , set ] means ( $3 in NAT & ( for n1, n2, m being Element of NAT st n1 = $2 & n2 = $3 & n2 <= m holds
S . m <> S . n1 ) );
A4: for z being set st z in rng S holds
ex n0 being Element of NAT st
for m being Element of NAT st n0 <= m holds
z <> S . m

let z be set ; :: thesis:
defpred S₂[ set ] means $1 = z;
assume A5: z in rng S ; :: thesis:
then reconsider z9 = z as Point of T ;
assume for n0 being Element of NAT ex m being Element of NAT st
( n0 <= m & z = S . m ) ; :: thesis:
then A6: for n being Element of NAT ex m being Element of NAT st
( n <= m & S₂[S . m] ) ;
ex S1 being subsequence of S st
for n being Element of NAT holds S₂[S1 . n] from VALUED_1:sch 1(A6);
then x in Cl {z9} by A3, Th15, Th34;
then z9 in Y by A1;
hence contradiction by A2, A5, XBOOLE_0:def 4; :: thesis:

end;

A7: for n being Nat
for z1 being set ex z2 being set st S₁[n,z1,z2]

let n be Nat; :: thesis:
let z1 be set ; :: thesis:

take 0 ; :: thesis:
thus 0 in NAT ; :: thesis:
let n1, n2, m be Element of NAT ; :: thesis:
assume that
A9: n1 = z1 and
n2 = 0 and
n2 <= m ; :: thesis:
thus S . m <> S . n1 by A8, A9; :: thesis:

end;

then z1 in dom S by NORMSP_1:12;
then S . z1 in rng S by FUNCT_1:def 3;
then consider n0 being Element of NAT such that
A10: for m being Element of NAT st n0 <= m holds
S . z1 <> S . m by A4;
take n0 ; :: thesis:
thus n0 in NAT ; :: thesis:
let n1, n2, m be Element of NAT ; :: thesis:
assume ( n1 = z1 & n2 = n0 & n2 <= m ) ; :: thesis:
hence S . m <> S . n1 by A10; :: thesis:

end;

consider f being Function such that
A11: dom f = NAT and
A12: f . 0 = 0 and
A13: for n being Nat holds S₁[n,f . n,f . (n + 1)] from RECDEF_1:sch 1(A7);
A14: for n being Nat holds f . n is Element of NAT

end;

then 0 < n by NAT_1:3;
then 0 + 1 < n + 1 by XREAL_1:6;
then 1 <= n by NAT_1:13;
then reconsider n1 = n - 1 as Element of NAT by INT_1:5, A15;
n1 + 1 = n ;
hence f . n is Element of NAT by A13; :: thesis:

end;

let n be Nat; :: according to SEQM_3:def 6 :: thesis:
reconsider nn = n, nn1 = n + 1 as Element of NAT by ORDINAL1:def 12;
reconsider n2 = f . nn1 as Element of NAT by A14;
reconsider n1 = f . nn as Element of NAT by A14;
assume f . n >= f . (n + 1) ; :: thesis:
then n2 <= n1 ;
then S . n1 <> S . n1 by A13;
hence contradiction ; :: thesis:

end;

then reconsider f = f as increasing sequence of NAT by A14, SEQM_3:13;
take S1 = S * f; :: thesis:
A16: for n1, n2 being Element of NAT st n1 < n2 holds
S1 . n1 <> S1 . n2

let n1, n2 be Element of NAT ; :: thesis:
reconsider n19 = f . n1 as Element of NAT ;
n2 in NAT ;
then n2 in dom S1 by NORMSP_1:12;
then A17: S . (f . n2) = S1 . n2 by FUNCT_1:12;
assume n1 < n2 ; :: thesis:
then A18: n1 + 1 <= n2 by NAT_1:13;
f . (n1 + 1) <= f . n2

hence f . (n1 + 1) <= f . n2 ; :: thesis:

end;

end;

end;

let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis:
assume that
A20: x1 in dom S1 and
A21: x2 in dom S1 and
A22: S1 . x1 = S1 . x2 ; :: thesis:
reconsider n2 = x2 as Element of NAT by A21;
reconsider n1 = x1 as Element of NAT by A20;
assume A23: x1 <> x2 ; :: thesis:

end;

end;