let N be Element of NAT ; :: thesis:
let F be sequence of (TOP-REAL N); :: thesis:
let x be Point of (TOP-REAL N); :: thesis:
let x' be Point of (Euclid N); :: thesis:
assume A1: x = x' ; :: thesis:

hereby :: thesis:

assume A2: x is_a_cluster_point_of F ; :: thesis:
let r be real number ; :: thesis:
let n be Element of NAT ; :: thesis:
assume A3: r > 0 ; :: thesis:
reconsider O = Ball x',r as open Subset of (TOP-REAL N) by Th30;
x in O by A1, A3, GOBOARD6:4;
then consider m being Element of NAT such that
A4: ( n <= m & F . m in O ) by A2, FRECHET2:def 4;
reconsider m = m as Element of NAT ;
take m = m; :: thesis:
thus ( n <= m & F . m in Ball x',r ) by A4; :: thesis:

end;

assume A5: for r being real number
for n being Element of NAT st r > 0 holds
ex m being Element of NAT st
( n <= m & F . m in Ball x',r ) ; :: thesis:
for O being Subset of (TOP-REAL N)
for n being Element of NAT st O is open & x in O holds
ex m being Element of NAT st
( n <= m & F . m in O )

proof

let O be Subset of (TOP-REAL N); :: thesis:
let n be Element of NAT ; :: thesis:
assume A6: ( O is open & x in O ) ; :: thesis:
X: TopStruct(# the carrier of (TOP-REAL N),the topology of (TOP-REAL N) #) = TopSpaceMetr (Euclid N) by EUCLID:def 8;
then reconsider G' = O as Subset of (TopSpaceMetr (Euclid N)) ;
G' is open by PRE_TOPC:60, X, A6;
then consider r being real number such that
A7: ( r > 0 & Ball x',r c= G' ) by A1, A6, TOPMETR:22;
reconsider n' = n as Element of NAT ;
consider m being Element of NAT such that
A8: ( n' <= m & F . m in Ball x',r ) by A5, A7;
take m ; :: thesis:
thus ( n <= m & F . m in O ) by A7, A8; :: thesis:

end;

hence x is_a_cluster_point_of F by FRECHET2:def 4; :: thesis: