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 Def7;
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 Def7;
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:24;
reconsider x9 = x as Point of R^1 by A3, TOPMETR:24;
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:24;
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 13;
then A10: A /\ D <> {} by XBOOLE_0:def 7;
A9 /\ B9 <> {}

proof

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

proof

assume a in {REAL } ; :: thesis:
then a = REAL by TARSKI:def 1;
hence contradiction by A13; :: thesis:

end;

a in A by A10, XBOOLE_0:def 4;
then a 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 13;
then consider S9 being sequence of R^1 such that
A15: rng S9 c= A9 and
A16: x9 in Lim S9 by Def5;
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, Def4;
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, Def2;
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 Def4; :: 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:37;
hence rng S c= A by FUNCOP_1:14; :: thesis:
S is_convergent_to x by Th23;
hence x in Lim S by Def4; :: 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:24;
reconsider k99 = k as Point of (TopSpaceMetr RealSpace ) ;
reconsider k9 = k99 as Point of RealSpace by TOPMETR:16;
set Bs = Balls k99;
consider h being Function of NAT ,(Balls k99) such that
A32: 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;
A33: 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 ;
A34: 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:78;
then A35: H /\ A9 <> {} by A29, A34, YELLOW_8:21;
then z in H by XBOOLE_0:def 4;
hence ( z in the carrier of R^1 & S₂[n,z] ) by A35; :: thesis:

end;

consider S9 being Function such that
A36: ( dom S9 = NAT & rng S9 c= the carrier of R^1 ) and
A37: for n being set st n in NAT holds
S₂[n,S9 . n] from WELLORD2:sch 1(A33);
reconsider S9 = S9 as Function of NAT ,the carrier of R^1 by A36, FUNCT_2:4;
A38: 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
A39: r > 0 and
A40: Ball k9,r c= U1 by TOPMETR:22;
reconsider r = r as Real by XREAL_0:def 1;
consider n being Element of NAT such that
A41: 1 / n < r and
A42: n > 0 by A39, 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 A37;
then A43: 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 A42, XREAL_1:90;
then Ball k9,(1 / (m + 1)) c= Ball k9,r by A41, PCOMPS_1:1, XXREAL_0:2;
then A44: Ball k9,(1 / (m + 1)) c= U1 by A40, XBOOLE_1:1;
h . m = Ball k9,(1 / (m + 1)) by A32;
hence S9 . m in U1 by A44, A43; :: 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
A45: z9 in dom S9 and
A46: z = S9 . z9 by FUNCT_1:def 5;
S9 . z9 in (h . z9) /\ A9 by A37, A45;
hence z in A9 by A46, XBOOLE_0:def 4; :: thesis:

end;

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

end;

consider g being Function such that
A47: ( 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
A48: k in dom g and
A49: z = g . k by FUNCT_1:def 5;
g . k in the topology of R^1 by A47, A48;
hence z in bool the carrier of R^1 by A49; :: 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
A50: k in dom g and
A51: O = g . k by FUNCT_1:def 5;
g . k in the topology of R^1 by A47, A50;
hence O is open by A51, PRE_TOPC:def 5; :: thesis:

end;

then A52: union F is open by TOPS_2:26;
(union F) \ NAT c= REAL \ NAT by TOPMETR:24, 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 Def7;
reconsider B = B as Subset of REAL? ;
A53: B /\ A = {}

proof

consider z being Element of B /\ A;
assume A54: B /\ A <> {} ; :: thesis:
then A55: z in B by XBOOLE_0:def 4;
A56: z in A by A54, XBOOLE_0:def 4;

per cases by A55, XBOOLE_0:def 3;

suppose z in (union F) \ NAT ; :: thesis:

then z in union F by XBOOLE_0:def 5;
then consider C being set such that
A57: z in C and
A58: C in F by TARSKI:def 4;
consider l being set such that
A59: l in dom g and
A60: C = g . l by A58, FUNCT_1:def 5;
(g . l) /\ A = {} by A47, A59;
hence contradiction by A56, A57, A60, XBOOLE_0:def 4; :: thesis:

end;

suppose z in {REAL } ; :: thesis:

then z = REAL by TARSKI:def 1;
hence contradiction by A25, A54, 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 A47, FUNCT_1:def 5;
hence k in union F by TARSKI:def 4; :: thesis:

end;

then ( B is open & REAL in B ) by A52, Th31;
then A meets B by A1, A25, PRE_TOPC:def 13;
hence contradiction by A53, XBOOLE_0:def 7; :: 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, Th31;
consider n being Element of NAT such that
A67: for m being Element of NAT st n <= m holds
S9 . m in O by A61, A64, A65, Def2;
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 A68: S9 . m in O by A67;
m in NAT ;
then m in dom S9 by NORMSP_1:17;
then S9 . m in rng S9 by FUNCT_1:def 5;
then S9 . m in A9 by A63;
then S9 . m in the carrier of REAL? ;
then S9 . m in (REAL \ NAT ) \/ {REAL } by Def7;
then A69: ( S9 . m in REAL \ NAT or S9 . m in {REAL } ) by XBOOLE_0:def 3;
S9 . m <> REAL

proof

A70: S9 . m in REAL by TOPMETR:24;
assume S9 . m = REAL ; :: thesis:
hence contradiction by A70; :: thesis:

end;

then not S9 . m in NAT by A69, 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 Def4; :: thesis:

end;