let X be set ; :: thesis: for B being non-empty ManySortedSet of X st rng B c= bool (bool X) & ( for x, U being set st x in X & U in B . x holds

x in U ) & ( 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 ) ) & ( 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 ) ) holds

ex P being Subset-Family of X st

( P = Union B & ( for T being TopStruct st the carrier of T = X & the topology of T = UniCl P holds

( T is TopSpace & ( for T9 being non empty TopSpace st T9 = T holds

B is Neighborhood_System of T9 ) ) ) )

let B be non-empty ManySortedSet of X; :: thesis: ( rng B c= bool (bool X) & ( for x, U being set st x in X & U in B . x holds

x in U ) & ( 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 ) ) & ( 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 ) ) implies ex P being Subset-Family of X st

( P = Union B & ( for T being TopStruct st the carrier of T = X & the topology of T = UniCl P holds

( T is TopSpace & ( for T9 being non empty TopSpace st T9 = T holds

B is Neighborhood_System of T9 ) ) ) ) )

assume A1: rng B c= bool (bool X) ; :: thesis: ( ex x, U being set st

( x in X & U in B . x & not x in U ) or ex x, y, U being set st

( x in U & U in B . y & y in X & ( for V being set holds

( not V in B . x or not V c= U ) ) ) or ex x, U1, U2 being set st

( x in X & U1 in B . x & U2 in B . x & ( for U being set holds

( not U in B . x or not U c= U1 /\ U2 ) ) ) or ex P being Subset-Family of X st

( P = Union B & ( for T being TopStruct st the carrier of T = X & the topology of T = UniCl P holds

( T is TopSpace & ( for T9 being non empty TopSpace st T9 = T holds

B is Neighborhood_System of T9 ) ) ) ) )

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: ( ex x, y, U being set st

( x in U & U in B . y & y in X & ( for V being set holds

( not V in B . x or not V c= U ) ) ) or ex x, U1, U2 being set st

( x in X & U1 in B . x & U2 in B . x & ( for U being set holds

( not U in B . x or not U c= U1 /\ U2 ) ) ) or ex P being Subset-Family of X st

( P = Union B & ( for T being TopStruct st the carrier of T = X & the topology of T = UniCl P holds

( T is TopSpace & ( for T9 being non empty TopSpace st T9 = T holds

B is Neighborhood_System of T9 ) ) ) ) )

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: ( ex x, U1, U2 being set st

( x in X & U1 in B . x & U2 in B . x & ( for U being set holds

( not U in B . x or not U c= U1 /\ U2 ) ) ) or ex P being Subset-Family of X st

( P = Union B & ( for T being TopStruct st the carrier of T = X & the topology of T = UniCl P holds

( T is TopSpace & ( for T9 being non empty TopSpace st T9 = T holds

B is Neighborhood_System of T9 ) ) ) ) )

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: ex P being Subset-Family of X st

( P = Union B & ( for T being TopStruct st the carrier of T = X & the topology of T = UniCl P holds

( T is TopSpace & ( for T9 being non empty TopSpace st T9 = T holds

B is Neighborhood_System of T9 ) ) ) )

A6: P is point-filtered

( T is TopSpace & ( for T9 being non empty TopSpace st T9 = T holds

B is Neighborhood_System of T9 ) ) ) )

thus P = Union B ; :: thesis: for T being TopStruct st the carrier of T = X & the topology of T = UniCl P holds

( T is TopSpace & ( for T9 being non empty TopSpace st T9 = T holds

B is Neighborhood_System of T9 ) )

let T be TopStruct ; :: thesis: ( the carrier of T = X & the topology of T = UniCl P implies ( T is TopSpace & ( for T9 being non empty TopSpace st T9 = T holds

B is Neighborhood_System of T9 ) ) )

assume that

A19: the carrier of T = X and

A20: the topology of T = UniCl P ; :: thesis: ( T is TopSpace & ( for T9 being non empty TopSpace st T9 = T holds

B is Neighborhood_System of T9 ) )

hence T is TopSpace by A19, A20, A6, Th2; :: thesis: for T9 being non empty TopSpace st T9 = T holds

B is Neighborhood_System of T9

let T9 be non empty TopSpace; :: thesis: ( T9 = T implies B is Neighborhood_System of T9 )

assume A23: T9 = T ; :: thesis: B is Neighborhood_System of T9

then reconsider B9 = B as ManySortedSet of T9 by A19;

B9 is Neighborhood_System of T9

x in U ) & ( 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 ) ) & ( 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 ) ) holds

ex P being Subset-Family of X st

( P = Union B & ( for T being TopStruct st the carrier of T = X & the topology of T = UniCl P holds

( T is TopSpace & ( for T9 being non empty TopSpace st T9 = T holds

B is Neighborhood_System of T9 ) ) ) )

let B be non-empty ManySortedSet of X; :: thesis: ( rng B c= bool (bool X) & ( for x, U being set st x in X & U in B . x holds

x in U ) & ( 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 ) ) & ( 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 ) ) implies ex P being Subset-Family of X st

( P = Union B & ( for T being TopStruct st the carrier of T = X & the topology of T = UniCl P holds

( T is TopSpace & ( for T9 being non empty TopSpace st T9 = T holds

B is Neighborhood_System of T9 ) ) ) ) )

assume A1: rng B c= bool (bool X) ; :: thesis: ( ex x, U being set st

( x in X & U in B . x & not x in U ) or ex x, y, U being set st

( x in U & U in B . y & y in X & ( for V being set holds

( not V in B . x or not V c= U ) ) ) or ex x, U1, U2 being set st

( x in X & U1 in B . x & U2 in B . x & ( for U being set holds

( not U in B . x or not U c= U1 /\ U2 ) ) ) or ex P being Subset-Family of X st

( P = Union B & ( for T being TopStruct st the carrier of T = X & the topology of T = UniCl P holds

( T is TopSpace & ( for T9 being non empty TopSpace st T9 = T holds

B is Neighborhood_System of T9 ) ) ) ) )

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: ( ex x, y, U being set st

( x in U & U in B . y & y in X & ( for V being set holds

( not V in B . x or not V c= U ) ) ) or ex x, U1, U2 being set st

( x in X & U1 in B . x & U2 in B . x & ( for U being set holds

( not U in B . x or not U c= U1 /\ U2 ) ) ) or ex P being Subset-Family of X st

( P = Union B & ( for T being TopStruct st the carrier of T = X & the topology of T = UniCl P holds

( T is TopSpace & ( for T9 being non empty TopSpace st T9 = T holds

B is Neighborhood_System of T9 ) ) ) ) )

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: ( ex x, U1, U2 being set st

( x in X & U1 in B . x & U2 in B . x & ( for U being set holds

( not U in B . x or not U c= U1 /\ U2 ) ) ) or ex P being Subset-Family of X st

( P = Union B & ( for T being TopStruct st the carrier of T = X & the topology of T = UniCl P holds

( T is TopSpace & ( for T9 being non empty TopSpace st T9 = T holds

B is Neighborhood_System of T9 ) ) ) ) )

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: ex P being Subset-Family of X st

( P = Union B & ( for T being TopStruct st the carrier of T = X & the topology of T = UniCl P holds

( T is TopSpace & ( for T9 being non empty TopSpace st T9 = T holds

B is Neighborhood_System of T9 ) ) ) )

A6: P is point-filtered

proof

take
P
; :: thesis: ( P = Union B & ( for T being TopStruct st the carrier of T = X & the topology of T = UniCl P holds
let x, U1, U2 be set ; :: according to TOPGEN_3:def 1 :: thesis: ( U1 in P & U2 in P & x in U1 /\ U2 implies ex U being Subset of X st

( U in P & x in U & U c= U1 /\ U2 ) )

assume that

A7: U1 in P and

A8: U2 in P and

A9: x in U1 /\ U2 ; :: thesis: ex U being Subset of X st

( U in P & x in U & U c= U1 /\ U2 )

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: ( U in P & x in U & U c= U1 /\ U2 )

thus U in P by A2, A16, A17, CARD_5:2; :: thesis: ( x in U & U c= U1 /\ U2 )

thus x in U by A3, A16, A17; :: thesis: U c= U1 /\ U2

V1 /\ V2 c= U1 /\ U2 by A15, A12, XBOOLE_1:27;

hence U c= U1 /\ U2 by A18; :: thesis: verum

end;( U in P & x in U & U c= U1 /\ U2 ) )

assume that

A7: U1 in P and

A8: U2 in P and

A9: x in U1 /\ U2 ; :: thesis: ex U being Subset of X st

( U in P & x in U & U c= U1 /\ U2 )

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: ( U in P & x in U & U c= U1 /\ U2 )

thus U in P by A2, A16, A17, CARD_5:2; :: thesis: ( x in U & U c= U1 /\ U2 )

thus x in U by A3, A16, A17; :: thesis: U c= U1 /\ U2

V1 /\ V2 c= U1 /\ U2 by A15, A12, XBOOLE_1:27;

hence U c= U1 /\ U2 by A18; :: thesis: verum

( T is TopSpace & ( for T9 being non empty TopSpace st T9 = T holds

B is Neighborhood_System of T9 ) ) ) )

thus P = Union B ; :: thesis: for T being TopStruct st the carrier of T = X & the topology of T = UniCl P holds

( T is TopSpace & ( for T9 being non empty TopSpace st T9 = T holds

B is Neighborhood_System of T9 ) )

let T be TopStruct ; :: thesis: ( the carrier of T = X & the topology of T = UniCl P implies ( T is TopSpace & ( for T9 being non empty TopSpace st T9 = T holds

B is Neighborhood_System of T9 ) ) )

assume that

A19: the carrier of T = X and

A20: the topology of T = UniCl P ; :: thesis: ( T is TopSpace & ( for T9 being non empty TopSpace st T9 = T holds

B is Neighborhood_System of T9 ) )

now :: thesis: for x being set st x in X holds

ex U being Subset of X st

( U in P & x in U )

then
P is covering
by Th1;ex U being Subset of X st

( U in P & x in U )

let x be set ; :: thesis: ( x in X implies ex U being Subset of X st

( U in P & x in U ) )

set U = the Element of B . x;

assume A21: x in X ; :: thesis: ex U being Subset of X st

( U in P & x in U )

then A22: the Element of B . x in P by A2, CARD_5:2;

x in the Element of B . x by A3, A21;

hence ex U being Subset of X st

( U in P & x in U ) by A22; :: thesis: verum

end;( U in P & x in U ) )

set U = the Element of B . x;

assume A21: x in X ; :: thesis: ex U being Subset of X st

( U in P & x in U )

then A22: the Element of B . x in P by A2, CARD_5:2;

x in the Element of B . x by A3, A21;

hence ex U being Subset of X st

( U in P & x in U ) by A22; :: thesis: verum

hence T is TopSpace by A19, A20, A6, Th2; :: thesis: for T9 being non empty TopSpace st T9 = T holds

B is Neighborhood_System of T9

let T9 be non empty TopSpace; :: thesis: ( T9 = T implies B is Neighborhood_System of T9 )

assume A23: T9 = T ; :: thesis: B is Neighborhood_System of T9

then reconsider B9 = B as ManySortedSet of T9 by A19;

B9 is Neighborhood_System of T9

proof

hence
B is Neighborhood_System of T9
; :: thesis: verum
let x be Point of T9; :: according to TOPGEN_2:def 3 :: thesis: B9 . x is Element of bool (bool the carrier of T9)

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

end;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

proof

hence
B9 . x is Element of bool (bool the carrier of T9)
; :: thesis: verum
A25:
P c= UniCl P
by CANTOR_1:1;

Bx c= P by A24, ZFMISC_1:74;

then Bx c= the topology of T9 by A25, A20, A23;

then A26: Bx is open by TOPS_2:64;

Bx is x -quasi_basis

end;Bx c= P by A24, ZFMISC_1:74;

then Bx c= the topology of T9 by A25, A20, A23;

then A26: Bx is open by TOPS_2:64;

Bx is x -quasi_basis

proof

hence
Bx is Basis of x
by A26; :: thesis: verum
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: for b_{1} being Element of bool the carrier of T9 holds

( not b_{1} is open or not x in b_{1} or ex b_{2} being Element of bool the carrier of T9 st

( b_{2} in Bx & b_{2} c= b_{1} ) )

let A be Subset of T9; :: thesis: ( not A is open or not x in A or ex b_{1} being Element of bool the carrier of T9 st

( b_{1} in Bx & b_{1} c= A ) )

assume A in the topology of T9 ; :: according to PRE_TOPC:def 2 :: thesis: ( not x in A or ex b_{1} being Element of bool the carrier of T9 st

( b_{1} in Bx & b_{1} c= A ) )

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: ex b_{1} being Element of bool the carrier of T9 st

( b_{1} in Bx & b_{1} c= A )

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_{1} being Element of bool the carrier of T9 st

( b_{1} in Bx & b_{1} c= A )
by A31, XBOOLE_1:1; :: thesis: verum

end;x in a by A3, A19, A23;

hence x in Intersect Bx by SETFAM_1:43; :: according to YELLOW_8:def 1 :: thesis: for b

( not b

( b

let A be Subset of T9; :: thesis: ( not A is open or not x in A or ex b

( b

assume A in the topology of T9 ; :: according to PRE_TOPC:def 2 :: thesis: ( not x in A or ex b

( b

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: ex b

( b

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

( b