let N be Nat; :: thesis: for F being sequence of (TOP-REAL N)
for x being Point of (TOP-REAL N)
for x9 being Point of (Euclid N) st x = x9 holds
( x is_a_cluster_point_of F iff for r being Real
for n being Nat st r > 0 holds
ex m being Nat st
( n <= m & F . m in Ball (x9,r) ) )
let F be sequence of (TOP-REAL N); :: thesis: for x being Point of (TOP-REAL N)
for x9 being Point of (Euclid N) st x = x9 holds
( x is_a_cluster_point_of F iff for r being Real
for n being Nat st r > 0 holds
ex m being Nat st
( n <= m & F . m in Ball (x9,r) ) )
let x be Point of (TOP-REAL N); :: thesis: for x9 being Point of (Euclid N) st x = x9 holds
( x is_a_cluster_point_of F iff for r being Real
for n being Nat st r > 0 holds
ex m being Nat st
( n <= m & F . m in Ball (x9,r) ) )
let x9 be Point of (Euclid N); :: thesis: ( x = x9 implies ( x is_a_cluster_point_of F iff for r being Real
for n being Nat st r > 0 holds
ex m being Nat st
( n <= m & F . m in Ball (x9,r) ) ) )
assume A1: x = x9 ; :: thesis: ( x is_a_cluster_point_of F iff for r being Real
for n being Nat st r > 0 holds
ex m being Nat st
( n <= m & F . m in Ball (x9,r) ) )

hereby :: thesis: ( ( for r being Real
for n being Nat st r > 0 holds
ex m being Nat st
( n <= m & F . m in Ball (x9,r) ) ) implies x is_a_cluster_point_of F )

assume A2: x is_a_cluster_point_of F ; :: thesis: for r being Real
for n being Nat st r > 0 holds
ex m being Nat st
( n <= m & F . m in Ball (x9,r) )
let r be Real; :: thesis: for n being Nat st r > 0 holds
ex m being Nat st
( n <= m & F . m in Ball (x9,r) )
let n be Nat; :: thesis: ( r > 0 implies ex m being Nat st
( n <= m & F . m in Ball (x9,r) ) )
reconsider O = Ball (x9,r) as open Subset of (TOP-REAL N) by Th1;
assume r > 0 ; :: thesis: ex m being Nat st
( n <= m & F . m in Ball (x9,r) )
then x in O by A1, GOBOARD6:1;
then consider m being Element of NAT such that
A3: ( n <= m & F . m in O ) by A2, FRECHET2:def 3;
reconsider m = m as Nat ;
take m = m; :: thesis: ( n <= m & F . m in Ball (x9,r) )
thus ( n <= m & F . m in Ball (x9,r) ) by A3; :: thesis: verum

end;

assume A4: for r being Real
for n being Nat st r > 0 holds
ex m being Nat st
( n <= m & F . m in Ball (x9,r) ) ; :: thesis: x is_a_cluster_point_of F
for O being Subset of (TOP-REAL N)
for n being 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: for n being Nat st O is open & x in O holds
ex m being Element of NAT st
( n <= m & F . m in O )
let n be Nat; :: thesis: ( O is open & x in O implies ex m being Element of NAT st
( n <= m & F . m in O ) )
assume that
A5: O is open and
A6: x in O ; :: thesis: ex m being Element of NAT st
( n <= m & F . m in O )
reconsider n9 = n as Nat ;
A7: TopStruct(# the carrier of (TOP-REAL N), the topology of (TOP-REAL N) #) = TopSpaceMetr (Euclid N) by EUCLID:def 8;
then reconsider G9 = O as Subset of (TopSpaceMetr (Euclid N)) ;
G9 is open by A5, A7, PRE_TOPC:30;
then consider r being Real such that
A8: r > 0 and
A9: Ball (x9,r) c= G9 by A1, A6, TOPMETR:15;
consider m being Nat such that
A10: ( n9 <= m & F . m in Ball (x9,r) ) by A4, A8;
reconsider m = m as Element of NAT by ORDINAL1:def 12;
take m ; :: thesis: ( n <= m & F . m in O )
thus ( n <= m & F . m in O ) by A9, A10; :: thesis: verum

end;

hence x is_a_cluster_point_of F by FRECHET2:def 3; :: thesis: verum