let T be non empty finite-weight TopSpace; :: thesis:
consider B being Basis of T such that
A1: card B = weight T by WAYBEL23:75;
weight T is finite by Def4;
then A2: B is finite by A1;
deffunc H₁( set ) -> set = meet { U where U is Subset of T : ( $1 in U & U in B ) } ;

A3: now

let a be set ; :: thesis:
assume a in the carrier of T ; :: thesis:
then reconsider x = a as Point of T ;
set S = { U where U is Subset of T : ( x in U & U in B ) } ;
B c= the topology of T by CANTOR_1:def 2;
then FinMeetCl B c= FinMeetCl the topology of T by CANTOR_1:16;
then A4: FinMeetCl B c= the topology of T by CANTOR_1:5;
consider U being Subset of T such that
A5: ( U in B & x in U ) and
U c= [#] T by YELLOW_9:31;
A6: { U where U is Subset of T : ( x in U & U in B ) } c= B

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume a in { U where U is Subset of T : ( x in U & U in B ) } ; :: thesis:
then ex U being Subset of T st
( a = U & x in U & U in B ) ;
hence a in B ; :: thesis:

end;

then reconsider S = { U where U is Subset of T : ( x in U & U in B ) } as Subset-Family of T by XBOOLE_1:1;
S is finite by A2, A6;
then ( Intersect S in FinMeetCl B & U in S ) by A5, A6, CANTOR_1:def 4;
then ( Intersect S in the topology of T & S <> {} ) by A4;
hence H₁(a) in the topology of T by SETFAM_1:def 10; :: thesis:

end;

consider f being Function of the carrier of T,the topology of T such that
A7: for a being set st a in the carrier of T holds
f . a = H₁(a) from FUNCT_2:sch 2(A3);
set B0 = rng f;
reconsider B0 = rng f as Subset-Family of T by XBOOLE_1:1;

A8: now

let a be set ; :: thesis:
assume a in the carrier of T ; :: thesis:
then reconsider x = a as Point of T ;
set S = { U where U is Subset of T : ( x in U & U in B ) } ;
consider U being Subset of T such that
A9: ( U in B & x in U ) and
U c= [#] T by YELLOW_9:31;
A10: ( U in { U where U is Subset of T : ( x in U & U in B ) } & f . a = meet { U where U is Subset of T : ( x in U & U in B ) } ) by A7, A9;

let b be set ; :: thesis:
assume b in { U where U is Subset of T : ( x in U & U in B ) } ; :: thesis:
then ex U being Subset of T st
( b = U & a in U & U in B ) ;
hence a in b ; :: thesis:

end;

hence a in f . a by A10, SETFAM_1:def 1; :: thesis:

end;

A11: now

let x be Point of T; :: thesis:
let V be Subset of T; :: thesis:
set S = { U where U is Subset of T : ( x in U & U in B ) } ;
assume ( x in V & V is open ) ; :: thesis:
then consider U being Subset of T such that
A12: ( U in B & x in U & U c= V ) by YELLOW_9:31;
( U in { U where U is Subset of T : ( x in U & U in B ) } & f . x = meet { U where U is Subset of T : ( x in U & U in B ) } ) by A7, A12;
then f . x c= U by SETFAM_1:4;
hence f . x c= V by A12, XBOOLE_1:1; :: thesis:

end;

now

let A be Subset of T; :: thesis:
assume A13: A is open ; :: thesis:
let p be Point of T; :: thesis:
assume A14: p in A ; :: thesis:
f . p in the topology of T ;
then reconsider a = f . p as Subset of T ;
take a = a; :: thesis:
thus a in B0 by FUNCT_2:6; :: thesis:
thus p in a by A8; :: thesis:
thus a c= A by A11, A13, A14; :: thesis:

end;

then reconsider B0 = B0 as Basis of T by YELLOW_9:32;
take B0 ; :: thesis:
take f ; :: thesis:
thus B0 = rng f ; :: thesis:
let x be Point of T; :: thesis:
thus ( x in f . x & ( for U being open Subset of T st x in U holds
f . x c= U ) ) by A8, A11; :: thesis: