let T be non empty TopSpace; :: thesis:
assume A1: T is first-countable ; :: thesis:
let A be Subset of T; :: according to FRECHET:def 6 :: thesis:
let x be Point of T; :: thesis:
assume A2: x in Cl A ; :: thesis:
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 A3, CARD_3:96;
defpred S₁[ 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 & S₁[n,y] )

defpred S₂[ Nat] means ex H being Subset of T st
( H = meet (f .: (succ $1)) & H is open );
let n be object ; :: thesis:
A6: for n being Nat st S₂[n] holds
S₂[n + 1]

let n be Nat; :: thesis:
given G being Subset of T such that A7: G = meet (f .: (succ n)) and
A8: G is open ; :: thesis:
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 FUNCT_2:def 1, ORDINAL1:6;
then A11: f . n in f .: (succ n) by FUNCT_1:def 6, A10;
f . (n + 1) in B ;
then consider H1 being Subset of T such that
A12: H1 = f . (n + 1) ;
A13: H1 is open by A12, YELLOW_8:12;
consider H being Subset of T such that
A14: H = H1 /\ G ;
take H ; :: thesis:
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 A9, FUNCT_1:59
.= (meet {(f . (n + 1))}) /\ (meet (f .: (succ n))) by A11, SETFAM_1:9
.= H by A7, A12, A14, SETFAM_1:10 ;
hence ( H = meet (f .: (succ (n + 1))) & H is open ) by A8, A13, A14, TOPS_1:11; :: thesis:

end;

assume n in NAT ; :: thesis:
then reconsider n = n as Element of NAT ;
A15: S₂[ 0 ]

f . 0 in B ;
then reconsider H = f . 0 as Subset of T ;
take H ; :: thesis:
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 .: (succ 0)) & H is open ) by YELLOW_8:12; :: thesis:

end;

let G be set ; :: thesis:
assume G in f .: (succ n) ; :: thesis:
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 A18, FUNCT_2:5;
hence x in G by A19, YELLOW_8:12; :: thesis:

end;

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
S₁[n,S . n] ) ) from FUNCT_1:sch 6(A5);
A22: rng S c= A

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in rng S ; :: thesis:
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;
S₁[a,S . a] by A21, A23;
then y in A /\ (meet (f .: (succ a))) by A23;
hence y in A by XBOOLE_0:def 4; :: thesis:

end;

reconsider S = S as sequence of T by A21, FUNCT_2:def 1, RELSET_1:4;
A24: for m, n being Nat st n <= m holds
A /\ (meet (f .: (succ m))) c= A /\ (meet (f .: (succ n)))

end;

let U1 be Subset of T; :: according to FRECHET:def 3 :: thesis:
assume A27: ( U1 is open & x in U1 ) ; :: thesis:
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 A27, YELLOW_8:13;
consider n being object such that
A30: n in dom f and
A31: U2 = f . n by A4, A28, FUNCT_1:def 3;
reconsider n = n as Element of NAT by A30;
for m being Nat st n <= m holds
S . m in U1

end;

hence ex n being Nat st
for m being Nat st n <= m holds
S . m in U1 ; :: thesis:

end;