let X be set ; :: thesis:
let B be non-empty ManySortedSet of ; :: thesis:
assume A1: rng B c= bool (bool X) ; :: thesis:
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;
A2: dom B = X by PARTFUN1:def 4;
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:
A6: P is point-filtered

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

end;

take P ; :: thesis:
thus P = Union B ; :: thesis:
let T be TopStruct ; :: thesis:
assume that
A19: the carrier of T = X and
A20: the topology of T = UniCl P ; :: thesis:

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

end;

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

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

A25: P c= UniCl P by CANTOR_1:1;
Bx c= P by A24, ZFMISC_1:92;
hence Bx c= the topology of T' by A25, A20, A23, XBOOLE_1:1; :: according to YELLOW_8:def 2 :: thesis:
for a being set st a in Bx holds
x in a by A3, A19, A23;
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
A26: Y c= P and
A27: A = union Y by A19, A20, A23, CANTOR_1:def 1;
assume x in A ; :: thesis:
then consider a being set such that
A28: x in a and
A29: a in Y by A27, TARSKI:def 4;
ex b being set st
( b in dom B & a in B . b ) by A26, A29, CARD_5:10;
then A30: ex V being set st
( V in B . x & V c= a ) by A2, A4, A28;
a c= A by A27, A29, ZFMISC_1:92;
hence ex b₁ being Element of bool the carrier of T' st
( b₁ in Bx & b₁ c= A ) by A30, XBOOLE_1:1; :: thesis:

end;

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

end;

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