let A be Subset of REAL?; :: according to FRECHET:def 6 :: thesis:
let x be Point of REAL?; :: thesis:
assume A1: x in Cl A ; :: thesis:
x in the carrier of REAL? ;
then x in (REAL \ NAT) \/ {REAL} by Def8;
then A2: ( x in REAL \ NAT or x in {REAL} ) by XBOOLE_0:def 3;

per cases by A2, TARSKI:def 1;

suppose A3: x in REAL \ NAT ; :: thesis:

then A4: x in REAL ;
A c= the carrier of REAL? ;
then A5: A c= (REAL \ NAT) \/ {REAL} by Def8;
A \ {REAL} c= REAL

proof

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume A6: a in A \ {REAL} ; :: thesis:
then a in A by XBOOLE_0:def 5;
then ( a in REAL \ NAT or a in {REAL} ) by A5, XBOOLE_0:def 3;
hence a in REAL by A6, XBOOLE_0:def 5; :: thesis:

end;

then reconsider A9 = A \ {REAL} as Subset of R^1 by TOPMETR:17;
reconsider x9 = x as Point of R^1 by A3, TOPMETR:17;
reconsider A9 = A9 as Subset of R^1 ;
for B9 being Subset of R^1 st B9 is open & x9 in B9 holds
A9 meets B9

proof

reconsider C = NAT as Subset of R^1 by TOPMETR:17, NUMBERS:19;
let B9 be Subset of R^1; :: thesis:
reconsider B1 = B9 as Subset of R^1 ;
reconsider C = C as Subset of R^1 ;
A7: not x9 in NAT by A3, XBOOLE_0:def 5;
B9 \ NAT misses NAT by XBOOLE_1:79;
then A8: (B9 \ NAT) /\ NAT = {} ;
then reconsider D = B1 \ C as Subset of REAL? by Th29;
assume B9 is open ; :: thesis:
then B1 \ C is open by Th4, Th10;
then A9: D is open by A8, Th30;
reconsider D = D as Subset of REAL? ;
assume x9 in B9 ; :: thesis:
then x9 in B9 \ NAT by A7, XBOOLE_0:def 5;
then A meets D by A1, A9, PRE_TOPC:def 7;
then A10: A /\ D <> {} ;
A9 /\ B9 <> {}

proof

set a = the Element of A /\ D;
A11: the Element of A /\ D in D by A10, XBOOLE_0:def 4;
then A12: the Element of A /\ D in B9 by XBOOLE_0:def 5;
A13: the Element of A /\ D in REAL by A11, TOPMETR:17;
A14: not the Element of A /\ D in {REAL}

proof

assume the Element of A /\ D in {REAL} ; :: thesis:
then the Element of A /\ D = REAL by TARSKI:def 1;
hence contradiction by A13; :: thesis:

end;

the Element of A /\ D in A by A10, XBOOLE_0:def 4;
then the Element of A /\ D in A \ {REAL} by A14, XBOOLE_0:def 5;
hence A9 /\ B9 <> {} by A12, XBOOLE_0:def 4; :: thesis:

end;

hence A9 meets B9 ; :: thesis:

end;

then x9 in Cl A9 by PRE_TOPC:def 7;
then consider S9 being sequence of R^1 such that
A15: rng S9 c= A9 and
A16: x9 in Lim S9 by Def6;
A17: rng S9 c= A by A15, XBOOLE_0:def 5;
then reconsider S = S9 as sequence of REAL? by Th2, XBOOLE_1:1;
take S ; :: thesis:
thus rng S c= A by A17; :: thesis:
A18: S9 is_convergent_to x9 by A16, Def5;
S is_convergent_to x

proof

reconsider C = {REAL} as Subset of REAL? by Lm3;
let V be Subset of REAL?; :: according to FRECHET:def 3 :: thesis:
assume that
A19: V is open and
A20: x in V ; :: thesis:
reconsider C = C as Subset of REAL? ;
REAL in {REAL} by TARSKI:def 1;
then A21: not REAL in V \ {REAL} by XBOOLE_0:def 5;
then reconsider V9 = V \ C as Subset of R^1 by Th29;
V \ C is open by A19, Th4, Th31;
then A22: V9 is open by A21, Th30;
not x in C

proof

assume x in C ; :: thesis:
then x = REAL by TARSKI:def 1;
hence contradiction by A4; :: thesis:

end;

then x in V \ C by A20, XBOOLE_0:def 5;
then consider n being Nat such that
A23: for m being Nat st n <= m holds
S9 . m in V9 by A18, A22;
take n ; :: thesis:
let m be Nat; :: thesis:
assume n <= m ; :: thesis:
then S9 . m in V9 by A23;
hence S . m in V by XBOOLE_0:def 5; :: thesis:

end;

hence x in Lim S by Def5; :: thesis:

end;

suppose A24: ( x = REAL & x in A ) ; :: thesis:

reconsider S = NAT --> x as sequence of REAL? ;
take S ; :: thesis:
{x} c= A by A24, ZFMISC_1:31;
hence rng S c= A by FUNCOP_1:8; :: thesis:
S is_convergent_to x by Th22;
hence x in Lim S by Def5; :: thesis:

end;

suppose A25: ( x = REAL & not x in A ) ; :: thesis:

then reconsider A9 = A as Subset of R^1 by Th29;
ex k being Point of R^1 st
( k in NAT & ex S9 being sequence of R^1 st
( rng S9 c= A9 & S9 is_convergent_to k ) )

proof

defpred S₁[ object , object ] means ex D2 being set st
( D2 = $2 & $1 in D2 & $2 in the topology of R^1 & D2 /\ A9 = {} );
assume A26: for k being Point of R^1 holds
( not k in NAT or for S9 being sequence of R^1 holds
( not rng S9 c= A9 or not S9 is_convergent_to k ) ) ; :: thesis:
A27: for k being object st k in NAT holds
ex U1 being object st S₁[k,U1]

proof

given k being object such that A28: k in NAT and
A29: for U1 being object holds not S₁[k,U1] ; :: thesis:
reconsider k = k as Point of R^1 by A28, TOPMETR:17, NUMBERS:19;
reconsider k99 = k as Point of (TopSpaceMetr RealSpace) ;
reconsider k9 = k99 as Point of RealSpace by TOPMETR:12;
set Bs = Balls k99;
consider h being sequence of (Balls k99) such that
A30: for n being Element of NAT holds h . n = Ball (k9,(1 / (n + 1))) by Th11;
defpred S₂[ object , object ] means $2 in (h . $1) /\ A9;
A31: for n being object st n in NAT holds
ex z being object st
( z in the carrier of R^1 & S₂[n,z] )

proof

let n be object ; :: thesis:
assume n in NAT ; :: thesis:
then reconsider n = n as Element of NAT ;
A32: h . n in Balls k99 ;
then reconsider H = h . n as Subset of R^1 ;
take z = the Element of H /\ A9; :: thesis:
Balls k99 c= the topology of R^1 by TOPS_2:64;
then A33: H /\ A9 <> {} by A29, A32, YELLOW_8:12;
then z in H by XBOOLE_0:def 4;
hence ( z in the carrier of R^1 & S₂[n,z] ) by A33; :: thesis:

end;

consider S9 being Function such that
A34: ( dom S9 = NAT & rng S9 c= the carrier of R^1 ) and
A35: for n being object st n in NAT holds
S₂[n,S9 . n] from FUNCT_1:sch 6(A31);
reconsider S9 = S9 as sequence of the carrier of R^1 by A34, FUNCT_2:2;
A36: S9 is_convergent_to k

proof

let U1 be Subset of R^1; :: according to FRECHET:def 3 :: thesis:
assume ( U1 is open & k in U1 ) ; :: thesis:
then consider r being Real such that
A37: r > 0 and
A38: Ball (k9,r) c= U1 by TOPMETR:15;
reconsider r = r as Real ;
consider n being Nat such that
A39: 1 / n < r and
A40: n > 0 by A37, Lm1;
reconsider n = n as Element of NAT by ORDINAL1:def 12;
take n ; :: thesis:
let m be Nat; :: thesis:
A41: m in NAT by ORDINAL1:def 12;
S9 . m in (h . m) /\ A9 by A35, A41;
then A42: S9 . m in h . m by XBOOLE_0:def 4;
assume n <= m ; :: thesis:
then n < m + 1 by NAT_1:13;
then 1 / (m + 1) < 1 / n by A40, XREAL_1:88;
then Ball (k9,(1 / (m + 1))) c= Ball (k9,r) by A39, PCOMPS_1:1, XXREAL_0:2;
then A43: Ball (k9,(1 / (m + 1))) c= U1 by A38;
h . m = Ball (k9,(1 / (m + 1))) by A30, A41;
hence S9 . m in U1 by A43, A42; :: thesis:

end;

rng S9 c= A9

proof

let z be object ; :: according to TARSKI:def 3 :: thesis:
assume z in rng S9 ; :: thesis:
then consider z9 being object such that
A44: z9 in dom S9 and
A45: z = S9 . z9 by FUNCT_1:def 3;
S9 . z9 in (h . z9) /\ A9 by A35, A44;
hence z in A9 by A45, XBOOLE_0:def 4; :: thesis:

end;

hence contradiction by A26, A28, A36; :: thesis:

end;

consider g being Function such that
A46: ( dom g = NAT & ( for k being object st k in NAT holds
S₁[k,g . k] ) ) from CLASSES1:sch 1(A27);
rng g c= bool the carrier of R^1

proof

let z be object ; :: according to TARSKI:def 3 :: thesis:
assume z in rng g ; :: thesis:
then consider k being object such that
A47: k in dom g and
A48: z = g . k by FUNCT_1:def 3;
S₁[k,g . k] by A46, A47;
then g . k in the topology of R^1 ;
hence z in bool the carrier of R^1 by A48; :: thesis:

end;

then reconsider F = rng g as Subset-Family of R^1 ;
F is open

proof

let O be Subset of R^1; :: according to TOPS_2:def 1 :: thesis:
assume O in F ; :: thesis:
then consider k being object such that
A49: k in dom g and
A50: O = g . k by FUNCT_1:def 3;
S₁[k,g . k] by A46, A49;
then g . k in the topology of R^1 ;
hence O is open by A50, PRE_TOPC:def 2; :: thesis:

end;

then A51: union F is open by TOPS_2:19;
(union F) \ NAT c= REAL \ NAT by TOPMETR:17, XBOOLE_1:33;
then ((union F) \ NAT) \/ {REAL} c= (REAL \ NAT) \/ {REAL} by XBOOLE_1:9;
then reconsider B = ((union F) \ NAT) \/ {REAL} as Subset of REAL? by Def8;
reconsider B = B as Subset of REAL? ;
A52: B /\ A = {}

proof

set z = the Element of B /\ A;
assume A53: B /\ A <> {} ; :: thesis:
then A54: the Element of B /\ A in B by XBOOLE_0:def 4;
A55: the Element of B /\ A in A by A53, XBOOLE_0:def 4;

per cases by A54, XBOOLE_0:def 3;

suppose the Element of B /\ A in (union F) \ NAT ; :: thesis:

then the Element of B /\ A in union F by XBOOLE_0:def 5;
then consider C being set such that
A56: the Element of B /\ A in C and
A57: C in F by TARSKI:def 4;
consider l being object such that
A58: l in dom g and
A59: C = g . l by A57, FUNCT_1:def 3;
S₁[l,g . l] by A46, A58;
then (g . l) /\ A = {} ;
hence contradiction by A55, A56, A59, XBOOLE_0:def 4; :: thesis:

end;

suppose the Element of B /\ A in {REAL} ; :: thesis:

then the Element of B /\ A = REAL by TARSKI:def 1;
hence contradiction by A25, A53, XBOOLE_0:def 4; :: thesis:

end;

NAT c= union F

proof

let k be object ; :: according to TARSKI:def 3 :: thesis:
assume A60: k in NAT ; :: thesis:
then S₁[k,g . k] by A46;
then ( k in g . k & g . k in rng g ) by A46, FUNCT_1:def 3, A60;
hence k in union F by TARSKI:def 4; :: thesis:

end;

then ( B is open & REAL in B ) by A51, Th28;
then A meets B by A1, A25, PRE_TOPC:def 7;
hence contradiction by A52; :: thesis:

end;

then consider k being Point of R^1 such that
A61: k in NAT and
A62: ex S9 being sequence of R^1 st
( rng S9 c= A9 & S9 is_convergent_to k ) ;
consider S9 being sequence of R^1 such that
A63: rng S9 c= A9 and
A64: S9 is_convergent_to k by A62;
reconsider S = S9 as sequence of REAL? by A63, Th2, XBOOLE_1:1;
take S ; :: thesis:
thus rng S c= A by A63; :: thesis:
S is_convergent_to x

proof

let U1 be Subset of REAL?; :: according to FRECHET:def 3 :: thesis:
assume ( U1 is open & x in U1 ) ; :: thesis:
then consider O being Subset of R^1 such that
A65: ( O is open & NAT c= O ) and
A66: U1 = (O \ NAT) \/ {REAL} by A25, Th28;
consider n being Nat such that
A67: for m being Nat st n <= m holds
S9 . m in O by A61, A64, A65;
take n ; :: thesis:
let m be Nat; :: thesis:
assume n <= m ; :: thesis:
then A68: S9 . m in O by A67;
A69: m in NAT by ORDINAL1:def 12;
then m in dom S9 by NORMSP_1:12;
then S9 . m in rng S9 by FUNCT_1:def 3;
then S9 . m in A9 by A63;
then S9 . m in the carrier of REAL? ;
then S9 . m in (REAL \ NAT) \/ {REAL} by Def8;
then A70: ( S9 . m in REAL \ NAT or S9 . m in {REAL} ) by XBOOLE_0:def 3;
reconsider m = m as Element of NAT by A69;
S9 . m <> REAL

proof

A71: S9 . m in REAL by TOPMETR:17;
assume S9 . m = REAL ; :: thesis:
hence contradiction by A71; :: thesis:

end;

then not S9 . m in NAT by A70, TARSKI:def 1, XBOOLE_0:def 5;
then S9 . m in O \ NAT by A68, XBOOLE_0:def 5;
hence S . m in U1 by A66, XBOOLE_0:def 3; :: thesis:

end;

hence x in Lim S by Def5; :: thesis:

end;