let X be set ; :: thesis:
let B be non-empty ManySortedSet of X; :: thesis:
assume A1: rng B c= bool (bool X) ; :: thesis:
Union B c= union (bool (bool X)) by A1, ZFMISC_1:77;
then reconsider P = Union B as Subset-Family of X by ZFMISC_1:81;
A2: dom B = X by PARTFUN1:def 2;
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 object st
( y2 in X & U2 in B . y2 ) by A2, A8, CARD_5:2;
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 object st
( y1 in X & U1 in B . y1 ) by A7, A2, CARD_5:2;
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 2;
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:2;
then reconsider U = U as Subset of X ;
take U ; :: thesis:
thus U in P by A2, A16, A17, CARD_5:2; :: 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; :: thesis:

end;

end;

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

for a being set st a in Bx holds
x in a by A3, A19, A23;
hence x in Intersect Bx by SETFAM_1:43; :: according to YELLOW_8:def 1 :: thesis:
let A be Subset of T9; :: thesis:
assume A in the topology of T9 ; :: according to PRE_TOPC:def 2 :: thesis:
then consider Y being Subset-Family of T9 such that
A27: Y c= P and
A28: A = union Y by A19, A20, A23, CANTOR_1:def 1;
assume x in A ; :: thesis:
then consider a being set such that
A29: x in a and
A30: a in Y by A28, TARSKI:def 4;
ex b being object st
( b in dom B & a in B . b ) by A27, A30, CARD_5:2;
then A31: ex V being set st
( V in B . x & V c= a ) by A4, A29;
a c= A by A28, A30, ZFMISC_1:74;
hence ex b₁ being Element of bool the carrier of T9 st
( b₁ in Bx & b₁ c= A ) by A31, XBOOLE_1:1; :: thesis:

end;

end;

hence B9 . x is Element of bool (bool the carrier of T9) ; :: thesis:

end;