let T be non empty TopSpace; :: thesis:
assume A1: T is first-countable ; :: thesis:
let x be Point of T; :: thesis:
consider B1 being Basis of x such that
A2: B1 is countable by A1;
consider f being sequence of B1 such that
A3: rng f = B1 by A2, CARD_3:96;
defpred S₁[ object , object ] means ex D1 being set st
( D1 = $1 & $2 = meet (f .: (succ D1)) );
A4: for n being object st n in NAT holds
ex A being object st S₁[n,A]

let n be object ; :: thesis:
reconsider D1 = n as set by TARSKI:1;
assume n in NAT ; :: thesis:
take A = meet (f .: (succ D1)); :: thesis:
thus S₁[n,A] ; :: thesis:

end;

consider S being Function such that
A5: dom S = NAT and
A6: for n being object st n in NAT holds
S₁[n,S . n] from CLASSES1:sch 1(A4);
A7: rng S c= bool the carrier of T

let A be object ; :: according to TARSKI:def 3 :: thesis:
assume A in rng S ; :: thesis:
then consider n being object such that
A8: ( n in dom S & A = S . n ) by FUNCT_1:def 3;
reconsider n = n as set by TARSKI:1;
reconsider fsuccn = f .: (succ n) as Subset-Family of T by XBOOLE_1:1;
S₁[n,S . n] by A5, A6, A8;
then consider D1 being set such that
A9: ( D1 = n & S . n = meet fsuccn ) ;
thus A in bool the carrier of T by A8, A9; :: thesis:

end;

then reconsider B = rng S as Subset-Family of T ;
reconsider B = B as Subset-Family of T ;
A10: ex A being set st A in B

end;

let A be set ; :: thesis:
assume A in B ; :: thesis:
then consider n being object such that
A12: n in dom S and
A13: A = S . n by FUNCT_1:def 3;
reconsider n = n as set by TARSKI:1;
( dom f = NAT & n in succ n ) by FUNCT_2:def 1, ORDINAL1:6;
then A14: f . n in f .: (succ n) by A5, A12, FUNCT_1:def 6;
A15: for A1 being set st A1 in f .: (succ n) holds
x in A1

let A1 be set ; :: thesis:
assume A1 in f .: (succ n) ; :: thesis:
then consider m being object such that
A16: m in dom f and
m in succ n and
A17: A1 = f . m by FUNCT_1:def 6;
f . m in rng f by A16, FUNCT_1:def 3;
then reconsider A2 = A1 as Subset of T by A3, A17;
reconsider A2 = A2 as Subset of T ;
A2 in B1 by A3, A16, A17, FUNCT_1:def 3;
hence x in A1 by YELLOW_8:12; :: thesis:

end;

end;

let A be object ; :: according to TARSKI:def 3 :: thesis:
assume A in B ; :: thesis:
then consider n being object such that
A20: n in dom S and
A21: A = S . n by FUNCT_1:def 3;
reconsider n9 = n as Element of NAT by A5, A20;
reconsider n = n as set by TARSKI:1;
reconsider C = f .: (succ n) as Subset-Family of T by XBOOLE_1:1;
A22: C is open by YELLOW_8:12;
succ n9 is finite ;
then f .: (succ n) is finite ;
then A23: meet C is open by A22, TOPS_2:20;
S₁[n,S . n] by A5, A6, A20;
then A = meet (f .: (succ n)) by A21;
hence A in the topology of T by A23; :: thesis:

end;

for O being Subset of T st O is open & x in O holds
ex A being Subset of T st
( A in B & A c= O )

let O be Subset of T; :: thesis:
assume ( O is open & x in O ) ; :: thesis:
then consider A1 being Subset of T such that
A24: A1 in B1 and
A25: A1 c= O by YELLOW_8:def 1;
consider n being object such that
A26: n in dom f and
A27: A1 = f . n by A3, A24, FUNCT_1:def 3;
reconsider n = n as set by TARSKI:1;
S . n in rng S by A5, A26, FUNCT_1:def 3;
then reconsider A = S . n as Subset of T by A7;
reconsider A = A as Subset of T ;
take A ; :: thesis:
thus A in B by A5, A26, FUNCT_1:def 3; :: thesis:
n in succ n by ORDINAL1:6;
then f . n in f .: (succ n) by A26, FUNCT_1:def 6;
then A28: meet (f .: (succ n)) c= A1 by A27, SETFAM_1:3;
S₁[n,S . n] by A26, A6;
then S . n c= A1 by A28;
hence A c= O by A25; :: thesis:

end;

then reconsider B = B as Basis of x by A19, A11, A18, TOPS_2:64, YELLOW_8:def 1;
take B ; :: thesis:
take S ; :: thesis:
thus dom S = NAT by A5; :: thesis:
thus rng S = B ; :: thesis:
for n, m being Element of NAT st m >= n holds
S . m c= S . n

end;