let n be Nat; :: thesis:
let r be Point of (TOP-REAL n); :: thesis:
let X be Subset of (TOP-REAL n); :: thesis:
reconsider r9 = r as Point of (Euclid n) by TOPREAL3:8;
defpred S₁[ object , object ] means ex z being Nat st
( $1 = z & $2 = the Element of X /\ (Ball (r9,(1 / (z + 1)))) );
assume A1: r in Cl X ; :: thesis:

let x be object ; :: thesis:
assume x in NAT ; :: thesis:
then reconsider k = x as Nat ;
set n1 = k + 1;
set oi = Ball (r9,(1 / (k + 1)));
reconsider oi = Ball (r9,(1 / (k + 1))) as open Subset of (TOP-REAL n) by Th1;
reconsider u = the Element of X /\ oi as object ;
take u = u; :: thesis:
dist (r9,r9) < 1 / (k + 1) by METRIC_1:1;
then r in oi by METRIC_1:11;
then X meets oi by A1, PRE_TOPC:24;
then not X /\ oi is empty ;
then u in X /\ oi ;
hence u in the carrier of (TOP-REAL n) ; :: thesis:
thus S₁[x,u] ; :: thesis:

end;

consider seq being Function such that
A3: ( dom seq = NAT & rng seq c= the carrier of (TOP-REAL n) ) and
A4: for x being object st x in NAT holds
S₁[x,seq . x] from FUNCT_1:sch 6(A2);
reconsider seq = seq as Real_Sequence of n by A3, FUNCT_2:def 1, RELSET_1:4;
take seq ; :: thesis:
thus rng seq c= X :: thesis:

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in rng seq ; :: thesis:
then consider x being object such that
A5: x in dom seq and
A6: seq . x = y by FUNCT_1:def 3;
consider k being Nat such that
x = k and
A7: seq . x = the Element of X /\ (Ball (r9,(1 / (k + 1)))) by A4, A5;
set n1 = k + 1;
reconsider oi = Ball (r9,(1 / (k + 1))) as open Subset of (TOP-REAL n) by Th1;
dist (r9,r9) < 1 / (k + 1) by METRIC_1:1;
then r in oi by METRIC_1:11;
then X meets oi by A1, PRE_TOPC:24;
then not X /\ oi is empty ;
hence y in X by A6, A7, XBOOLE_0:def 4; :: thesis:

end;

let p be Real; :: thesis:
set cp = [/(1 / p)\];
A9: 1 / p <= [/(1 / p)\] by INT_1:def 7;
assume A10: 0 < p ; :: thesis:
then A11: 0 < [/(1 / p)\] by INT_1:def 7;
then reconsider cp = [/(1 / p)\] as Element of NAT by INT_1:3;
reconsider cp = cp as Nat ;
take k = cp; :: thesis:
k < k + 1 by NAT_1:13;
then A12: 1 / (k + 1) < 1 / k by A11, XREAL_1:88;
1 / (1 / p) >= 1 / cp by A10, A9, XREAL_1:85;
then A13: 1 / (k + 1) < p by A12, XXREAL_0:2;
let m be Nat; :: thesis:
assume k <= m ; :: thesis:
then A14: k + 1 <= m + 1 by XREAL_1:6;
set m1 = m + 1;
1 / (m + 1) <= 1 / (k + 1) by A14, XREAL_1:85;
then A15: 1 / (m + 1) < p by A13, XXREAL_0:2;
set oi = Ball (r9,(1 / (m + 1)));
reconsider oi = Ball (r9,(1 / (m + 1))) as open Subset of (TOP-REAL n) by Th1;
dist (r9,r9) < 1 / (m + 1) by METRIC_1:1;
then r in oi by METRIC_1:11;
then X meets oi by A1, PRE_TOPC:24;
then A16: not X /\ oi is empty ;
m in NAT by ORDINAL1:def 12;
then ex m9 being Nat st
( m9 = m & seq . m = the Element of X /\ (Ball (r9,(1 / (m9 + 1)))) ) by A4;
then seq . m in oi by A16, XBOOLE_0:def 4;
hence |.((seq . m) - r).| < p by A15, Th2, XXREAL_0:2; :: thesis:

end;