let T be TopSpace; :: thesis: for B being Basis of T
for A being Subset of T holds
( A is open iff for p being Point of T st p in A holds
ex a being Subset of T st
( a in B & p in a & a c= A ) )
let K be Basis of T; :: thesis: for A being Subset of T holds
( A is open iff for p being Point of T st p in A holds
ex a being Subset of T st
( a in K & p in a & a c= A ) )
let A be Subset of T; :: thesis: ( A is open iff for p being Point of T st p in A holds
ex a being Subset of T st
( a in K & p in a & a c= A ) )

hereby :: thesis: ( ( for p being Point of T st p in A holds
ex a being Subset of T st
( a in K & p in a & a c= A ) ) implies A is open )

assume A is open ; :: thesis: for p being Point of T st p in A holds
ex a being Subset of T st
( a in K & p in a & a c= A )
then A1: A = union { G where G is Subset of T : ( G in K & G c= A ) } by YELLOW_8:18;
let p be Point of T; :: thesis: ( p in A implies ex a being Subset of T st
( a in K & p in a & a c= A ) )
assume p in A ; :: thesis: ex a being Subset of T st
( a in K & p in a & a c= A )
then consider Z being set such that
A2: ( p in Z & Z in { G where G is Subset of T : ( G in K & G c= A ) } ) by A1, TARSKI:def 4;
ex a being Subset of T st
( Z = a & a in K & a c= A ) by A2;
hence ex a being Subset of T st
( a in K & p in a & a c= A ) by A2; :: thesis: verum

end;

assume A3: for p being Point of T st p in A holds
ex a being Subset of T st
( a in K & p in a & a c= A ) ; :: thesis: A is open
set F = { G where G is Subset of T : ( G in K & G c= A ) } ;
{ G where G is Subset of T : ( G in K & G c= A ) } c= bool the carrier of T

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { G where G is Subset of T : ( G in K & G c= A ) } or x in bool the carrier of T )
assume x in { G where G is Subset of T : ( G in K & G c= A ) } ; :: thesis: x in bool the carrier of T
then ex G being Subset of T st
( x = G & G in K & G c= A ) ;
hence x in bool the carrier of T ; :: thesis: verum

end;

then reconsider F = { G where G is Subset of T : ( G in K & G c= A ) } as Subset-Family of T ;
reconsider F = F as Subset-Family of T ;
A4: F is open

proof

let x be Subset of T; :: according to TOPS_2:def 1 :: thesis: ( not x in F or x is open )
assume x in F ; :: thesis: x is open
then ex G being Subset of T st
( x = G & G in K & G c= A ) ;
then ( x in K & K c= the topology of T ) by CANTOR_1:def 2;
hence x in the topology of T ; :: according to PRE_TOPC:def 5 :: thesis: verum

end;

A = union F

proof

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: union F c= A

let x be set ; :: thesis: ( x in A implies x in union F )
assume A5: x in A ; :: thesis: x in union F
then reconsider p = x as Point of T ;
consider a being Subset of T such that
A6: ( a in K & p in a & a c= A ) by A3, A5;
a in F by A6;
hence x in union F by A6, TARSKI:def 4; :: thesis: verum

end;

F c= bool A

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in F or x in bool A )
assume x in F ; :: thesis: x in bool A
then ex G being Subset of T st
( x = G & G in K & G c= A ) ;
hence x in bool A ; :: thesis: verum

end;

then union F c= union (bool A) by ZFMISC_1:95;
hence union F c= A by ZFMISC_1:99; :: thesis: verum

end;

hence A is open by A4, TOPS_2:26; :: thesis: verum