let T be non empty TopSpace; :: thesis: ( T is first-countable implies T is Frechet )
assume A1: T is first-countable ; :: thesis: T is Frechet
let A be Subset of T; :: according to FRECHET:def 6 :: thesis: for x being Point of T st x in Cl A holds
ex S being sequence of T st
( rng S c= A & x in Lim S )

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

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

consider B being Basis of x such that
A3: B is countable by A1;
consider f being sequence of B such that
A4: rng f = B by ;
defpred S1[ object , object ] means ex D1 being set st
( D1 = \$1 & \$2 in A /\ (meet (f .: (succ D1))) );
A5: for n being object st n in NAT holds
ex y being object st
( y in the carrier of T & S1[n,y] )
proof
defpred S2[ Nat] means ex H being Subset of T st
( H = meet (f .: (succ \$1)) & H is open );
let n be object ; :: thesis: ( n in NAT implies ex y being object st
( y in the carrier of T & S1[n,y] ) )

A6: for n being Nat st S2[n] holds
S2[n + 1]
proof
let n be Nat; :: thesis: ( S2[n] implies S2[n + 1] )
given G being Subset of T such that A7: G = meet (f .: (succ n)) and
A8: G is open ; :: thesis: S2[n + 1]
n + 1 in NAT ;
then A9: n + 1 in dom f by FUNCT_2:def 1;
A10: n in NAT by ORDINAL1:def 12;
( n in succ n & dom f = NAT ) by ;
then A11: f . n in f .: (succ n) by ;
f . (n + 1) in B ;
then consider H1 being Subset of T such that
A12: H1 = f . (n + 1) ;
A13: H1 is open by ;
consider H being Subset of T such that
A14: H = H1 /\ G ;
take H ; :: thesis: ( H = meet (f .: (succ (n + 1))) & H is open )
meet (f .: (succ (n + 1))) = meet (f .: ({(n + 1)} \/ (Segm (n + 1))))
.= meet (f .: ({(n + 1)} \/ (succ (Segm n)))) by NAT_1:38
.= meet ((Im (f,(n + 1))) \/ (f .: (succ n))) by RELAT_1:120
.= meet ({(f . (n + 1))} \/ (f .: (succ n))) by
.= (meet {(f . (n + 1))}) /\ (meet (f .: (succ n))) by
.= H by ;
hence ( H = meet (f .: (succ (n + 1))) & H is open ) by ; :: thesis: verum
end;
assume n in NAT ; :: thesis: ex y being object st
( y in the carrier of T & S1[n,y] )

then reconsider n = n as Element of NAT ;
A15: S2[ 0 ]
proof
f . 0 in B ;
then reconsider H = f . 0 as Subset of T ;
take H ; :: thesis: ( H = meet (f .: ()) & H is open )
0 in NAT ;
then 0 in dom f by FUNCT_2:def 1;
then meet (Im (f,0)) = meet {(f . 0)} by FUNCT_1:59
.= H by SETFAM_1:10 ;
hence ( H = meet (f .: ()) & H is open ) by YELLOW_8:12; :: thesis: verum
end;
for n being Nat holds S2[n] from NAT_1:sch 2(A15, A6);
then A16: ex H being Subset of T st
( H = meet (f .: (succ n)) & H is open ) ;
A17: for G being set st G in f .: (succ n) holds
x in G
proof
let G be set ; :: thesis: ( G in f .: (succ n) implies x in G )
assume G in f .: (succ n) ; :: thesis: x in G
then consider k being object such that
A18: k in dom f and
k in succ n and
A19: G = f . k by FUNCT_1:def 6;
f . k in B by ;
hence x in G by ; :: thesis: verum
end;
( n in succ n & dom f = NAT ) by ;
then f . n in f .: (succ n) by FUNCT_1:def 6;
then x in meet (f .: (succ n)) by ;
then A meets meet (f .: (succ n)) by ;
then consider y being object such that
A20: y in A /\ (meet (f .: (succ n))) by XBOOLE_0:4;
take y ; :: thesis: ( y in the carrier of T & S1[n,y] )
thus ( y in the carrier of T & S1[n,y] ) by A20; :: thesis: verum
end;
consider S being Function such that
A21: ( dom S = NAT & rng S c= the carrier of T & ( for n being object st n in NAT holds
S1[n,S . n] ) ) from A22: rng S c= A
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng S or y in A )
assume y in rng S ; :: thesis: y in A
then consider a being object such that
A23: ( a in dom S & y = S . a ) by FUNCT_1:def 3;
reconsider a = a as set by TARSKI:1;
S1[a,S . a] by ;
then y in A /\ (meet (f .: (succ a))) by A23;
hence y in A by XBOOLE_0:def 4; :: thesis: verum
end;
reconsider S = S as sequence of T by ;
A24: for m, n being Nat st n <= m holds
A /\ (meet (f .: (succ m))) c= A /\ (meet (f .: (succ n)))
proof
let m, n be Nat; :: thesis: ( n <= m implies A /\ (meet (f .: (succ m))) c= A /\ (meet (f .: (succ n))) )
assume n <= m ; :: thesis: A /\ (meet (f .: (succ m))) c= A /\ (meet (f .: (succ n)))
then n + 1 <= m + 1 by XREAL_1:6;
then Segm (n + 1) c= Segm (m + 1) by NAT_1:39;
then succ (Segm n) c= Segm (m + 1) by NAT_1:38;
then succ (Segm n) c= succ (Segm m) by NAT_1:38;
then A25: f .: (succ n) c= f .: (succ m) by RELAT_1:123;
A26: n in NAT by ORDINAL1:def 12;
( n in succ n & dom f = NAT ) by ;
then f . n in f .: (succ n) by ;
then meet (f .: (succ m)) c= meet (f .: (succ n)) by ;
hence A /\ (meet (f .: (succ m))) c= A /\ (meet (f .: (succ n))) by XBOOLE_1:26; :: thesis: verum
end;
S is_convergent_to x
proof
let U1 be Subset of T; :: 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 A27: ( U1 is open & x in U1 ) ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
S . m in U1

reconsider U1 = U1 as Subset of T ;
consider U2 being Subset of T such that
A28: U2 in B and
A29: U2 c= U1 by ;
consider n being object such that
A30: n in dom f and
A31: U2 = f . n by ;
reconsider n = n as Element of NAT by A30;
for m being Nat st n <= m holds
S . m in U1
proof
let m be Nat; :: thesis: ( n <= m implies S . m in U1 )
A32: m in NAT by ORDINAL1:def 12;
( n in succ n & dom f = NAT ) by ;
then A33: f . n in f .: (succ n) by FUNCT_1:def 6;
assume n <= m ; :: thesis: S . m in U1
then A34: A /\ (meet (f .: (succ m))) c= A /\ (meet (f .: (succ n))) by A24;
S1[m,S . m] by ;
then S . m in A /\ (meet (f .: (succ m))) ;
then S . m in meet (f .: (succ n)) by ;
then S . m in f . n by ;
hence S . m in U1 by ; :: thesis: verum
end;
hence ex n being Nat st
for m being Nat st n <= m holds
S . m in U1 ; :: thesis: verum
end;
then x in Lim S by Def5;
hence ex S being sequence of T st
( rng S c= A & x in Lim S ) by A22; :: thesis: verum