let X be set ; :: thesis:
let B be non-empty ManySortedSet of ; :: thesis:
assume A1: rng B c= bool (bool X) ; :: thesis:
A2: ( dom B = X & union (rng B) = Union B ) by PARTFUN1:def 4;
Union B c= union (bool (bool X)) by A1, ZFMISC_1:95;
then reconsider P = Union B as Subset-Family of X by ZFMISC_1:99;
assume A3: for x, U being set st x in X & U in B . x holds
x in U ; :: thesis:
assume A4: for x, y, U being set st x in U & U in B . y & y in X holds
ex V being set st
( V in B . x & V c= U ) ; :: thesis:
assume A5: for x, U1, U2 being set st x in X & U1 in B . x & U2 in B . x holds
ex U being set st
( U in B . x & U c= U1 /\ U2 ) ; :: thesis:
take P ; :: thesis:
thus P = Union B ; :: thesis:
let T be TopStruct ; :: thesis:
assume A6: ( the carrier of T = X & the topology of T = UniCl P ) ; :: thesis:
A7: P is point-filtered

proof

let x, U1, U2 be set ; :: according to TOPGEN_3:def 1 :: thesis:
assume A8: ( U1 in P & U2 in P & x in U1 /\ U2 ) ; :: thesis:
then consider y1 being set such that
A9: ( y1 in X & U1 in B . y1 ) by A2, CARD_5:10;
consider y2 being set such that
A10: ( y2 in X & U2 in B . y2 ) by A2, A8, CARD_5:10;
x in U1 by A8, XBOOLE_0:def 4;
then consider V1 being set such that
A11: ( V1 in B . x & V1 c= U1 ) by A4, A9;
x in U2 by A8, XBOOLE_0:def 4;
then consider V2 being set such that
A12: ( V2 in B . x & V2 c= U2 ) by A4, A10;
A13: x in X by A2, A11, FUNCT_1:def 4;
then consider U being set such that
A14: ( U in B . x & U c= V1 /\ V2 ) by A5, A11, A12;
U in P by A2, A13, A14, CARD_5:10;
then reconsider U = U as Subset of X ;
take U ; :: thesis:
thus U in P by A2, A13, A14, CARD_5:10; :: thesis:
thus x in U by A3, A13, A14; :: thesis:
V1 /\ V2 c= U1 /\ U2 by A11, A12, XBOOLE_1:27;
hence U c= U1 /\ U2 by A14, XBOOLE_1:1; :: thesis:

end;

now

let x be set ; :: thesis:
consider U being Element of B . x;
assume A15: x in X ; :: thesis:
( x in U & U in P ) by A2, A3, A15, CARD_5:10;
hence ex U being Subset of X st
( U in P & x in U ) ; :: thesis:

end;

then P is covering by Th1;
hence T is TopSpace by A6, A7, Th2; :: thesis:
let T' be non empty TopSpace; :: thesis:
assume A16: T' = T ; :: thesis:
then reconsider B' = B as ManySortedSet of by A6;
B' is Neighborhood_System of T'

proof

let x be Point of T'; :: according to TOPGEN_2:def 3 :: thesis:
A17: B' . x in rng B by A2, A6, A16, FUNCT_1:def 5;
then reconsider Bx = B' . x as Subset-Family of T' by A1, A6, A16;
Bx is Basis of x

proof

( Bx c= P & P c= UniCl P ) by A17, CANTOR_1:1, ZFMISC_1:92;
hence Bx c= the topology of T' by A6, A16, XBOOLE_1:1; :: according to YELLOW_8:def 2 :: thesis:
for a being set st a in Bx holds
x in a by A3, A6, A16;
hence x in Intersect Bx by SETFAM_1:58; :: thesis:
let A be Subset of T'; :: thesis:
assume A in the topology of T' ; :: according to PRE_TOPC:def 5 :: thesis:
then consider Y being Subset-Family of T' such that
A18: ( Y c= P & A = union Y ) by A6, A16, CANTOR_1:def 1;
assume x in A ; :: thesis:
then consider a being set such that
A19: ( x in a & a in Y ) by A18, TARSKI:def 4;
ex b being set st
( b in dom B & a in B . b ) by A18, A19, CARD_5:10;
then consider V being set such that
A20: ( V in B . x & V c= a ) by A2, A4, A19;
( a c= A & P c= UniCl P & V in P ) by A2, A6, A16, A18, A19, A20, CANTOR_1:1, CARD_5:10, ZFMISC_1:92;
hence ex b₁ being Element of bool the carrier of T' st
( b₁ in Bx & b₁ c= A ) by A20, XBOOLE_1:1; :: thesis:

end;

hence B' . x is Basis of x ; :: thesis:

end;

hence B is Neighborhood_System of T' ; :: thesis: