let T be TopSpace; :: thesis:
let K be Basis of T; :: thesis:
let A be Subset of T; :: thesis:

assume A is open ; :: thesis:
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:
assume p in A ; :: thesis:
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:

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

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { G where G is Subset of T : ( G in K & G c= A ) } ; :: thesis:
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:

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

let x be Subset of T; :: according to TOPS_2:def 1 :: thesis:
assume x in F ; :: thesis:
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:

end;

let x be object ; :: thesis:
assume A7: x in A ; :: thesis:
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:

end;

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

end;

end;