assume A2: x is_a_cluster_point_of F ; :: thesis:
let r be Real; :: thesis:
let n be Nat; :: thesis:
reconsider O = Ball (x9,r) as open Subset of (TOP-REAL N) by Th1;
assume r > 0 ; :: thesis:
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:
thus ( n <= m & F . m in Ball (x9,r) ) by A3; :: thesis:

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:
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 )

let O be Subset of (TOP-REAL N); :: thesis:
let n be Nat; :: thesis:
assume that
A5: O is open and
A6: x in O ; :: thesis:
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:
thus ( n <= m & F . m in O ) by A9, A10; :: thesis:

end;