let TM be metrizable TopSpace; :: thesis:
set cTM = [#] TM;
set TOP = the topology of TM;
let Null be Subset of TM; :: thesis:
assume A1: TM | Null is second-countable ; :: thesis:

defpred S₁[ object , object ] means for p being Point of TM
for A being Subset of TM st $1 = [p,A] holds
( $2 in the topology of TM & ( not p in A implies $2 = {} TM ) & ( p in A implies ex W being open Subset of TM st
( W = $2 & p in W & W c= A & Null misses Fr W ) ) );
assume A2: ( Null is finite-ind & ind Null <= 0 ) ; :: thesis:
A3: for x being object st x in [:([#] TM), the topology of TM:] holds
ex y being object st S₁[x,y]

let x be object ; :: thesis:
assume x in [:([#] TM), the topology of TM:] ; :: thesis:
then consider p9, A9 being object such that
A4: p9 in [#] TM and
A5: A9 in the topology of TM and
A6: x = [p9,A9] by ZFMISC_1:def 2;
reconsider p9 = p9 as Point of TM by A4;
reconsider A9 = A9 as open Subset of TM by A5, PRE_TOPC:def 2;

take {} TM ; :: thesis:
let p be Point of TM; :: thesis:
let A be Subset of TM; :: thesis:
assume A8: x = [p,A] ; :: thesis:
p = p9 by A6, A8, XTUPLE_0:1;
hence ( {} TM in the topology of TM & ( not p in A implies {} TM = {} TM ) & ( p in A implies ex W being open Subset of TM st
( W = {} TM & p in W & W c= A & Null misses Fr W ) ) ) by A6, A7, A8, PRE_TOPC:def 2, XTUPLE_0:1; :: thesis:

end;

then consider W being open Subset of TM such that
A9: ( p9 in W & W c= A9 & Null misses Fr W ) by A1, A2, Th38;
take W ; :: thesis:
let p be Point of TM; :: thesis:
let A be Subset of TM; :: thesis:
assume x = [p,A] ; :: thesis:
then ( p = p9 & A = A9 ) by A6, XTUPLE_0:1;
hence ( W in the topology of TM & ( not p in A implies W = {} TM ) & ( p in A implies ex W being open Subset of TM st
( W = W & p in W & W c= A & Null misses Fr W ) ) ) by A9, PRE_TOPC:def 2; :: thesis:

end;

consider f being Function such that
A10: dom f = [:([#] TM), the topology of TM:] and
A11: for x being object st x in [:([#] TM), the topology of TM:] holds
S₁[x,f . x] from CLASSES1:sch 1(A3);
A12: rng f c= the topology of TM

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in rng f ; :: thesis:
then consider x being object such that
A13: x in dom f and
A14: f . x = y by FUNCT_1:def 3;
ex p, A being object st
( p in [#] TM & A in the topology of TM & x = [p,A] ) by A10, A13, ZFMISC_1:def 2;
hence y in the topology of TM by A10, A11, A13, A14; :: thesis:

end;

then reconsider RNG = rng f as Subset-Family of TM by XBOOLE_1:1;

let A be Subset of TM; :: thesis:
assume A is open ; :: thesis:
then A15: A in the topology of TM by PRE_TOPC:def 2;
let p be Point of TM; :: thesis:
assume A16: p in A ; :: thesis:
A17: [p,A] in [:([#] TM), the topology of TM:] by A15, A16, ZFMISC_1:87;
then consider W being open Subset of TM such that
A18: ( W = f . [p,A] & p in W & W c= A ) and
Null misses Fr W by A11, A16;
reconsider W = W as Subset of TM ;
take W = W; :: thesis:
thus ( W in RNG & p in W & W c= A ) by A10, A17, A18, FUNCT_1:def 3; :: thesis:

end;

then reconsider RNG = RNG as Basis of TM by A12, YELLOW_9:32;
take RNG = RNG; :: thesis:
let B be Subset of TM; :: thesis:
assume B in RNG ; :: thesis:
then consider x being object such that
A19: x in dom f and
A20: f . x = B by FUNCT_1:def 3;
consider p, A being object such that
A21: p in [#] TM and
A22: A in the topology of TM and
A23: x = [p,A] by A10, A19, ZFMISC_1:def 2;
reconsider A = A as set by TARSKI:1;

end;

end;

given B being Basis of TM such that A24: for A being Subset of TM st A in B holds
Null misses Fr A ; :: thesis:
for p being Point of TM
for U being open Subset of TM st p in U holds
ex W being open Subset of TM st
( p in W & W c= U & Null misses Fr W )

let p be Point of TM; :: thesis:
let U be open Subset of TM; :: thesis:
assume p in U ; :: thesis:
then consider a being Subset of TM such that
A25: a in B and
A26: ( p in a & a c= U ) by YELLOW_9:31;
B c= the topology of TM by TOPS_2:64;
then reconsider a = a as open Subset of TM by A25, PRE_TOPC:def 2;
take a ; :: thesis:
thus ( p in a & a c= U & Null misses Fr a ) by A24, A25, A26; :: thesis:

end;