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 set ; :: 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;
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 = {} by XBOOLE_0:def 7;
then reconsider D = B1 \ C as Subset of REAL? by Th32;
assume B9 is open ; :: thesis:
then B1 \ C is open by Th4, Th10;
then A9: D is open by A8, Th33;
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 <> {} by XBOOLE_0:def 7;
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 by XBOOLE_0:def 7; :: 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

proof

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume a in rng S9 ; :: thesis:
hence a in A by A15, XBOOLE_0:def 5; :: thesis:

end;

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 Th32;
V \ C is open by A19, Th4, Th34;
then A22: V9 is open by A21, Th33;
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 Element of NAT such that
A23: for m being Element of NAT st n <= m holds
S9 . m in V9 by A18, A22, Def3;
take n ; :: thesis:
thus for m being Element of NAT st n <= m holds
S . m in V :: thesis:

proof

let m be Element of 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 Th23;
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 Th32;
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₁[ set , set ] means ( $1 in $2 & $2 in the topology of R^1 & $2 /\ 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 set st k in NAT holds
ex U1 being set st S₁[k,U1]

proof

given k being set such that A28: k in NAT and
A29: for U1 being set st k in U1 & U1 in the topology of R^1 holds
not U1 /\ A9 = {} ; :: thesis:
reconsider k = k as Point of R^1 by A28, TOPMETR:17;
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 Function of NAT,(Balls k99) such that
A30: for n being Element of NAT holds h . n = Ball (k9,(1 / (n + 1))) by Th11;
defpred S₂[ set , set ] means $2 in (h . $1) /\ A9;
A31: for n being set st n in NAT holds
ex z being set st
( z in the carrier of R^1 & S₂[n,z] )

proof

let n be set ; :: 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 set st n in NAT holds
S₂[n,S9 . n] from FUNCT_1:sch 5(A31);
reconsider S9 = S9 as Function of NAT, 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 number such that
A37: r > 0 and
A38: Ball (k9,r) c= U1 by TOPMETR:15;
reconsider r = r as Real by XREAL_0:def 1;
consider n being Element of NAT such that
A39: 1 / n < r and
A40: n > 0 by A37, Lm1;
take n ; :: thesis:
thus for m being Element of NAT st n <= m holds
S9 . m in U1 :: thesis:

proof

let m be Element of NAT ; :: thesis:
S9 . m in (h . m) /\ A9 by A35;
then A41: 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 A42: Ball (k9,(1 / (m + 1))) c= U1 by A38, XBOOLE_1:1;
h . m = Ball (k9,(1 / (m + 1))) by A30;
hence S9 . m in U1 by A42, A41; :: thesis:

end;

rng S9 c= A9

proof

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

end;

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

end;

consider g being Function such that
A45: ( dom g = NAT & ( for k being set 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 set ; :: according to TARSKI:def 3 :: thesis:
assume z in rng g ; :: thesis:
then consider k being set such that
A46: k in dom g and
A47: z = g . k by FUNCT_1:def 3;
g . k in the topology of R^1 by A45, A46;
hence z in bool the carrier of R^1 by A47; :: 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 set such that
A48: k in dom g and
A49: O = g . k by FUNCT_1:def 3;
g . k in the topology of R^1 by A45, A48;
hence O is open by A49, PRE_TOPC:def 2; :: thesis:

end;

then A50: 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? ;
A51: B /\ A = {}

proof

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

per cases by A53, 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
A55: the Element of B /\ A in C and
A56: C in F by TARSKI:def 4;
consider l being set such that
A57: l in dom g and
A58: C = g . l by A56, FUNCT_1:def 3;
(g . l) /\ A = {} by A45, A57;
hence contradiction by A54, A55, A58, 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, A52, XBOOLE_0:def 4; :: thesis:

end;

NAT c= union F

proof

let k be set ; :: according to TARSKI:def 3 :: thesis:
assume k in NAT ; :: thesis:
then ( k in g . k & g . k in rng g ) by A45, FUNCT_1:def 3;
hence k in union F by TARSKI:def 4; :: thesis:

end;

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

end;

then consider k being Point of R^1 such that
A59: k in NAT and
A60: 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
A61: rng S9 c= A9 and
A62: S9 is_convergent_to k by A60;
reconsider S = S9 as sequence of REAL? by A61, Th2, XBOOLE_1:1;
take S ; :: thesis:
thus rng S c= A by A61; :: 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
A63: ( O is open & NAT c= O ) and
A64: U1 = (O \ NAT) \/ {REAL} by A25, Th31;
consider n being Element of NAT such that
A65: for m being Element of NAT st n <= m holds
S9 . m in O by A59, A62, A63, Def3;
take n ; :: thesis:
thus for m being Element of NAT st n <= m holds
S . m in U1 :: thesis:

proof

let m be Element of NAT ; :: thesis:
assume n <= m ; :: thesis:
then A66: S9 . m in O by A65;
m in NAT ;
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 A61;
then S9 . m in the carrier of REAL? ;
then S9 . m in (REAL \ NAT) \/ {REAL} by Def8;
then A67: ( S9 . m in REAL \ NAT or S9 . m in {REAL} ) by XBOOLE_0:def 3;
S9 . m <> REAL

proof

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

end;

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

end;

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

end;