let X be set ; :: thesis: for B being Subset-Family of X st B is point-filtered & B is covering holds

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

( T is TopSpace & B is Basis of T )

let B be Subset-Family of X; :: thesis: ( B is point-filtered & B is covering implies for T being TopStruct st the carrier of T = X & the topology of T = UniCl B holds

( T is TopSpace & B is Basis of T ) )

assume A1: ( B is point-filtered & B is covering ) ; :: thesis: for T being TopStruct st the carrier of T = X & the topology of T = UniCl B holds

( T is TopSpace & B is Basis of T )

let T be TopStruct ; :: thesis: ( the carrier of T = X & the topology of T = UniCl B implies ( T is TopSpace & B is Basis of T ) )

assume that

A2: the carrier of T = X and

A3: the topology of T = UniCl B ; :: thesis: ( T is TopSpace & B is Basis of T )

T is TopSpace-like

reconsider B9 = B as Subset-Family of T by A2;

B9 c= the topology of T by A3, CANTOR_1:1;

hence B is Basis of T by A2, A3, CANTOR_1:def 2, TOPS_2:64; :: thesis: verum

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

( T is TopSpace & B is Basis of T )

let B be Subset-Family of X; :: thesis: ( B is point-filtered & B is covering implies for T being TopStruct st the carrier of T = X & the topology of T = UniCl B holds

( T is TopSpace & B is Basis of T ) )

assume A1: ( B is point-filtered & B is covering ) ; :: thesis: for T being TopStruct st the carrier of T = X & the topology of T = UniCl B holds

( T is TopSpace & B is Basis of T )

let T be TopStruct ; :: thesis: ( the carrier of T = X & the topology of T = UniCl B implies ( T is TopSpace & B is Basis of T ) )

assume that

A2: the carrier of T = X and

A3: the topology of T = UniCl B ; :: thesis: ( T is TopSpace & B is Basis of T )

T is TopSpace-like

proof

hence
T is TopSpace
; :: thesis: B is Basis of T
union B in UniCl B
by CANTOR_1:def 1;

hence the carrier of T in the topology of T by A1, A2, A3, ABIAN:4; :: according to PRE_TOPC:def 1 :: thesis: ( ( for b_{1} being Element of bool (bool the carrier of T) holds

( not b_{1} c= the topology of T or union b_{1} in the topology of T ) ) & ( for b_{1}, b_{2} being Element of bool the carrier of T holds

( not b_{1} in the topology of T or not b_{2} in the topology of T or b_{1} /\ b_{2} in the topology of T ) ) )

set Bc = { c where c is Subset of T : ( c in B & c c= a /\ b ) } ;

{ c where c is Subset of T : ( c in B & c c= a /\ b ) } c= bool X

assume a in the topology of T ; :: thesis: ( not b in the topology of T or a /\ b in the topology of T )

then consider Ba being Subset-Family of T such that

A4: Ba c= B and

A5: a = union Ba by A2, A3, CANTOR_1:def 1;

assume b in the topology of T ; :: thesis: a /\ b in the topology of T

then consider Bb being Subset-Family of T such that

A6: Bb c= B and

A7: b = union Bb by A2, A3, CANTOR_1:def 1;

A8: union Bc = a /\ b

end;hence the carrier of T in the topology of T by A1, A2, A3, ABIAN:4; :: according to PRE_TOPC:def 1 :: thesis: ( ( for b

( not b

( not b

hereby :: thesis: for b_{1}, b_{2} being Element of bool the carrier of T holds

( not b_{1} in the topology of T or not b_{2} in the topology of T or b_{1} /\ b_{2} in the topology of T )

let a, b be Subset of T; :: thesis: ( not a in the topology of T or not b in the topology of T or a /\ b in the topology of T )( not b

let a be Subset-Family of T; :: thesis: ( a c= the topology of T implies union a in the topology of T )

assume a c= the topology of T ; :: thesis: union a in the topology of T

then union a in UniCl the topology of T by CANTOR_1:def 1;

hence union a in the topology of T by A2, A3, YELLOW_9:15; :: thesis: verum

end;assume a c= the topology of T ; :: thesis: union a in the topology of T

then union a in UniCl the topology of T by CANTOR_1:def 1;

hence union a in the topology of T by A2, A3, YELLOW_9:15; :: thesis: verum

set Bc = { c where c is Subset of T : ( c in B & c c= a /\ b ) } ;

{ c where c is Subset of T : ( c in B & c c= a /\ b ) } c= bool X

proof

then reconsider Bc = { c where c is Subset of T : ( c in B & c c= a /\ b ) } as Subset-Family of T by A2;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { c where c is Subset of T : ( c in B & c c= a /\ b ) } or x in bool X )

assume x in { c where c is Subset of T : ( c in B & c c= a /\ b ) } ; :: thesis: x in bool X

then ex c being Subset of T st

( x = c & c in B & c c= a /\ b ) ;

hence x in bool X ; :: thesis: verum

end;assume x in { c where c is Subset of T : ( c in B & c c= a /\ b ) } ; :: thesis: x in bool X

then ex c being Subset of T st

( x = c & c in B & c c= a /\ b ) ;

hence x in bool X ; :: thesis: verum

assume a in the topology of T ; :: thesis: ( not b in the topology of T or a /\ b in the topology of T )

then consider Ba being Subset-Family of T such that

A4: Ba c= B and

A5: a = union Ba by A2, A3, CANTOR_1:def 1;

assume b in the topology of T ; :: thesis: a /\ b in the topology of T

then consider Bb being Subset-Family of T such that

A6: Bb c= B and

A7: b = union Bb by A2, A3, CANTOR_1:def 1;

A8: union Bc = a /\ b

proof

Bc c= B
Bc c= bool (a /\ b)

hence union Bc c= a /\ b by ZFMISC_1:81; :: according to XBOOLE_0:def 10 :: thesis: a /\ b c= union Bc

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in a /\ b or x in union Bc )

assume A9: x in a /\ b ; :: thesis: x in union Bc

then x in a by XBOOLE_0:def 4;

then consider U1 being set such that

A10: x in U1 and

A11: U1 in Ba by A5, TARSKI:def 4;

x in b by A9, XBOOLE_0:def 4;

then consider U2 being set such that

A12: x in U2 and

A13: U2 in Bb by A7, TARSKI:def 4;

A14: U2 c= b by A7, A13, ZFMISC_1:74;

x in U1 /\ U2 by A10, A12, XBOOLE_0:def 4;

then consider U being Subset of X such that

A15: U in B and

A16: x in U and

A17: U c= U1 /\ U2 by A4, A11, A6, A13, A1;

U1 c= a by A5, A11, ZFMISC_1:74;

then U1 /\ U2 c= a /\ b by A14, XBOOLE_1:27;

then U c= a /\ b by A17;

then U in Bc by A2, A15;

hence x in union Bc by A16, TARSKI:def 4; :: thesis: verum

end;proof

then
union Bc c= union (bool (a /\ b))
by ZFMISC_1:77;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Bc or x in bool (a /\ b) )

assume x in Bc ; :: thesis: x in bool (a /\ b)

then ex c being Subset of T st

( x = c & c in B & c c= a /\ b ) ;

hence x in bool (a /\ b) ; :: thesis: verum

end;assume x in Bc ; :: thesis: x in bool (a /\ b)

then ex c being Subset of T st

( x = c & c in B & c c= a /\ b ) ;

hence x in bool (a /\ b) ; :: thesis: verum

hence union Bc c= a /\ b by ZFMISC_1:81; :: according to XBOOLE_0:def 10 :: thesis: a /\ b c= union Bc

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in a /\ b or x in union Bc )

assume A9: x in a /\ b ; :: thesis: x in union Bc

then x in a by XBOOLE_0:def 4;

then consider U1 being set such that

A10: x in U1 and

A11: U1 in Ba by A5, TARSKI:def 4;

x in b by A9, XBOOLE_0:def 4;

then consider U2 being set such that

A12: x in U2 and

A13: U2 in Bb by A7, TARSKI:def 4;

A14: U2 c= b by A7, A13, ZFMISC_1:74;

x in U1 /\ U2 by A10, A12, XBOOLE_0:def 4;

then consider U being Subset of X such that

A15: U in B and

A16: x in U and

A17: U c= U1 /\ U2 by A4, A11, A6, A13, A1;

U1 c= a by A5, A11, ZFMISC_1:74;

then U1 /\ U2 c= a /\ b by A14, XBOOLE_1:27;

then U c= a /\ b by A17;

then U in Bc by A2, A15;

hence x in union Bc by A16, TARSKI:def 4; :: thesis: verum

proof

hence
a /\ b in the topology of T
by A8, A2, A3, CANTOR_1:def 1; :: thesis: verum
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Bc or x in B )

assume x in Bc ; :: thesis: x in B

then ex c being Subset of T st

( x = c & c in B & c c= a /\ b ) ;

hence x in B ; :: thesis: verum

end;assume x in Bc ; :: thesis: x in B

then ex c being Subset of T st

( x = c & c in B & c c= a /\ b ) ;

hence x in B ; :: thesis: verum

reconsider B9 = B as Subset-Family of T by A2;

B9 c= the topology of T by A3, CANTOR_1:1;

hence B is Basis of T by A2, A3, CANTOR_1:def 2, TOPS_2:64; :: thesis: verum