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:9;
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 and
A3: 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 A3;
hence ex a being Subset of T st
( a in K & p in a & a c= A ) by A2; :: thesis: verum

end;

assume A4: 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 object ; :: 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 ;
A5: 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 A6: ex G being Subset of T st
( x = G & G in K & G c= A ) ;
K c= the topology of T by TOPS_2:64;
hence x in the topology of T by A6; :: according to PRE_TOPC:def 2 :: 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 object ; :: thesis: ( x in A implies x in union F )
assume A7: x in A ; :: thesis: x in union F
then reconsider p = x as Point of T ;
consider a being Subset of T such that
A8: a in K and
A9: p in a and
A10: a c= A by A4, A7;
a in F by A8, A10;
hence x in union F by A9, TARSKI:def 4; :: thesis: verum

end;

F c= bool A

proof

let x be object ; :: 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:77;
hence union F c= A by ZFMISC_1:81; :: thesis: verum

end;

hence A is open by A5, TOPS_2:19; :: thesis: verum