let A be Subset of REAL?; :: according to FRECHET:def 6 :: thesis: for x being Point of REAL? st x in Cl A holds
ex S being sequence of REAL? st
( rng S c= A & x in Lim S )

let x be Point of REAL?; :: thesis: ( x in Cl A implies ex S being sequence of REAL? st
( rng S c= A & x in Lim S ) )

assume A1: x in Cl A ; :: thesis: ex S being sequence of REAL? st
( rng S c= A & x in Lim S )

x in the carrier of REAL? ;
then x in () \/ by Def8;
then A2: ( x in REAL \ NAT or x in ) by XBOOLE_0:def 3;
per cases ( x in REAL \ NAT or ( x = REAL & x in A ) or ( x = REAL & not x in A ) ) by ;
suppose A3: x in REAL \ NAT ; :: thesis: ex S being sequence of REAL? st
( rng S c= A & x in Lim S )

then A4: x in REAL ;
A c= the carrier of REAL? ;
then A5: A c= () \/ by Def8;
A \ c= REAL
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in A \ or a in REAL )
assume A6: a in A \ ; :: thesis:
then a in A by XBOOLE_0:def 5;
then ( a in REAL \ NAT or a in ) by ;
hence a in REAL by ; :: thesis: verum
end;
then reconsider A9 = A \ as Subset of R^1 by TOPMETR:17;
reconsider x9 = x as Point of R^1 by ;
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 ;
let B9 be Subset of R^1; :: thesis: ( B9 is open & x9 in B9 implies A9 meets B9 )
reconsider B1 = B9 as Subset of R^1 ;
reconsider C = C as Subset of R^1 ;
A7: not x9 in NAT by ;
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: ( not x9 in B9 or A9 meets B9 )
then B1 \ C is open by ;
then A9: D is open by ;
reconsider D = D as Subset of REAL? ;
assume x9 in B9 ; :: thesis: A9 meets B9
then x9 in B9 \ NAT by ;
then A meets D by ;
then A10: A /\ D <> {} ;
A9 /\ B9 <> {}
proof
set a = the Element of A /\ D;
A11: the Element of A /\ D in D by ;
then A12: the Element of A /\ D in B9 by XBOOLE_0:def 5;
A13: the Element of A /\ D in REAL by ;
A14: not the Element of A /\ D in the Element of A /\ D in A by ;
then the Element of A /\ D in A \ by ;
hence A9 /\ B9 <> {} by ; :: thesis: verum
end;
hence A9 meets B9 ; :: thesis: verum
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 ;
then reconsider S = S9 as sequence of REAL? by ;
take S ; :: thesis: ( rng S c= A & x in Lim S )
thus rng S c= A by A17; :: thesis: x in Lim S
A18: S9 is_convergent_to x9 by ;
S is_convergent_to x
proof
reconsider C = as Subset of REAL? by Lm3;
let V be Subset of REAL?; :: according to FRECHET:def 3 :: thesis: ( V is open & x in V implies ex n being Nat st
for m being Nat st n <= m holds
S . m in V )

assume that
A19: V is open and
A20: x in V ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
S . m in V

reconsider C = C as Subset of REAL? ;
REAL in by TARSKI:def 1;
then A21: not REAL in V \ by XBOOLE_0:def 5;
then reconsider V9 = V \ C as Subset of R^1 by Th29;
V \ C is open by ;
then A22: V9 is open by ;
not x in C then x in V \ C by ;
then consider n being Nat such that
A23: for m being Nat st n <= m holds
S9 . m in V9 by ;
take n ; :: thesis: for m being Nat st n <= m holds
S . m in V

let m be Nat; :: thesis: ( n <= m implies S . m in V )
assume n <= m ; :: thesis: S . m in V
then S9 . m in V9 by A23;
hence S . m in V by XBOOLE_0:def 5; :: thesis: verum
end;
hence x in Lim S by Def5; :: thesis: verum
end;
suppose A24: ( x = REAL & x in A ) ; :: thesis: ex S being sequence of REAL? st
( rng S c= A & x in Lim S )

reconsider S = NAT --> x as sequence of REAL? ;
take S ; :: thesis: ( rng S c= A & x in Lim S )
{x} c= A by ;
hence rng S c= A by FUNCOP_1:8; :: thesis: x in Lim S
S is_convergent_to x by Th22;
hence x in Lim S by Def5; :: thesis: verum
end;
suppose A25: ( x = REAL & not x in A ) ; :: thesis: ex S being sequence of REAL? st
( rng S c= A & x in Lim S )

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 S1[ 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: contradiction
A27: for k being object st k in NAT holds
ex U1 being object st S1[k,U1]
proof
given k being object such that A28: k in NAT and
A29: for U1 being object holds not S1[k,U1] ; :: thesis: contradiction
reconsider k = k as Point of R^1 by ;
reconsider k99 = k as Point of ;
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 S2[ 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 & S2[n,z] )
proof
let n be object ; :: thesis: ( n in NAT implies ex z being object st
( z in the carrier of R^1 & S2[n,z] ) )

assume n in NAT ; :: thesis: ex z being object st
( z in the carrier of R^1 & S2[n,z] )

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: ( z in the carrier of R^1 & S2[n,z] )
Balls k99 c= the topology of R^1 by TOPS_2:64;
then A33: H /\ A9 <> {} by ;
then z in H by XBOOLE_0:def 4;
hence ( z in the carrier of R^1 & S2[n,z] ) by A33; :: thesis: verum
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
S2[n,S9 . n] from reconsider S9 = S9 as sequence of the carrier of R^1 by ;
A36: S9 is_convergent_to k
proof
let U1 be Subset of R^1; :: according to FRECHET:def 3 :: thesis: ( U1 is open & k in U1 implies ex n being Nat st
for m being Nat st n <= m holds
S9 . m in U1 )

assume ( U1 is open & k in U1 ) ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
S9 . m in U1

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 ;
reconsider n = n as Element of NAT by ORDINAL1:def 12;
take n ; :: thesis: for m being Nat st n <= m holds
S9 . m in U1

let m be Nat; :: thesis: ( n <= m implies S9 . m in U1 )
A41: m in NAT by ORDINAL1:def 12;
S9 . m in (h . m) /\ A9 by ;
then A42: S9 . m in h . m by XBOOLE_0:def 4;
assume n <= m ; :: thesis: S9 . m in U1
then n < m + 1 by NAT_1:13;
then 1 / (m + 1) < 1 / n by ;
then Ball (k9,(1 / (m + 1))) c= Ball (k9,r) by ;
then A43: Ball (k9,(1 / (m + 1))) c= U1 by A38;
h . m = Ball (k9,(1 / (m + 1))) by ;
hence S9 . m in U1 by ; :: thesis: verum
end;
rng S9 c= A9
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in rng S9 or z in A9 )
assume z in rng S9 ; :: thesis: z in A9
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 ;
hence z in A9 by ; :: thesis: verum
end;
hence contradiction by A26, A28, A36; :: thesis: verum
end;
consider g being Function such that
A46: ( dom g = NAT & ( for k being object st k in NAT holds
S1[k,g . k] ) ) from rng g c= bool the carrier of R^1
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in rng g or z in bool the carrier of R^1 )
assume z in rng g ; :: thesis: z in bool the carrier of R^1
then consider k being object such that
A47: k in dom g and
A48: z = g . k by FUNCT_1:def 3;
S1[k,g . k] by ;
then g . k in the topology of R^1 ;
hence z in bool the carrier of R^1 by A48; :: thesis: verum
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: ( not O in F or O is open )
assume O in F ; :: thesis: O is open
then consider k being object such that
A49: k in dom g and
A50: O = g . k by FUNCT_1:def 3;
S1[k,g . k] by ;
then g . k in the topology of R^1 ;
hence O is open by ; :: thesis: verum
end;
then A51: union F is open by TOPS_2:19;
(union F) \ NAT c= REAL \ NAT by ;
then ((union F) \ NAT) \/ c= () \/ by XBOOLE_1:9;
then reconsider B = (() \ NAT) \/ 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: contradiction
then A54: the Element of B /\ A in B by XBOOLE_0:def 4;
A55: the Element of B /\ A in A by ;
per cases ( the Element of B /\ A in () \ NAT or the Element of B /\ A in ) by ;
suppose the Element of B /\ A in () \ NAT ; :: thesis: contradiction
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 ;
S1[l,g . l] by ;
then (g . l) /\ A = {} ;
hence contradiction by A55, A56, A59, XBOOLE_0:def 4; :: thesis: verum
end;
suppose the Element of B /\ A in ; :: thesis: contradiction
end;
end;
end;
NAT c= union F
proof
let k be object ; :: according to TARSKI:def 3 :: thesis: ( not k in NAT or k in union F )
assume A60: k in NAT ; :: thesis: k in union F
then S1[k,g . k] by A46;
then ( k in g . k & g . k in rng g ) by ;
hence k in union F by TARSKI:def 4; :: thesis: verum
end;
then ( B is open & REAL in B ) by ;
then A meets B by ;
hence contradiction by A52; :: thesis: verum
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 ;
take S ; :: thesis: ( rng S c= A & x in Lim S )
thus rng S c= A by A63; :: thesis: x in Lim S
S is_convergent_to x
proof
let U1 be Subset of REAL?; :: according to FRECHET:def 3 :: thesis: ( U1 is open & x in U1 implies ex n being Nat st
for m being Nat st n <= m holds
S . m in U1 )

assume ( U1 is open & x in U1 ) ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
S . m in U1

then consider O being Subset of R^1 such that
A65: ( O is open & NAT c= O ) and
A66: U1 = (O \ NAT) \/ by ;
consider n being Nat such that
A67: for m being Nat st n <= m holds
S9 . m in O by ;
take n ; :: thesis: for m being Nat st n <= m holds
S . m in U1

let m be Nat; :: thesis: ( n <= m implies S . m in U1 )
assume n <= m ; :: thesis: S . m in U1
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 () \/ by Def8;
then A70: ( S9 . m in REAL \ NAT or S9 . m in ) by XBOOLE_0:def 3;
reconsider m = m as Element of NAT by A69;
S9 . m <> REAL then not S9 . m in NAT by ;
then S9 . m in O \ NAT by ;
hence S . m in U1 by ; :: thesis: verum
end;
hence x in Lim S by Def5; :: thesis: verum
end;
end;