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

proof

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₁ being Element of bool (bool the carrier of T) holds
( not b₁ c= the topology of T or union b₁ in the topology of T ) ) & ( for b₁, b₂ being Element of bool the carrier of T holds
( not b₁ in the topology of T or not b₂ in the topology of T or b₁ /\ b₂ in the topology of T ) ) )

hereby :: thesis: for b₁, b₂ being Element of bool the carrier of T holds
( not b₁ in the topology of T or not b₂ in the topology of T or b₁ /\ b₂ in the topology of T )

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;

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 )
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

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;

then reconsider Bc = { c where c is Subset of T : ( c in B & c c= a /\ b ) } as Subset-Family of T by A2;
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= bool (a /\ b)

proof

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;

then union Bc c= union (bool (a /\ b)) by ZFMISC_1:77;
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;

Bc c= B

proof

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;

hence a /\ b in the topology of T by A8, A2, A3, CANTOR_1:def 1; :: thesis: verum

end;

hence T is TopSpace ; :: thesis: B is Basis of T
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