defpred S_{1}[ set ] means ( T in the topology of T & x in T );

set IT = { S where S is Subset of T : S_{1}[S] } ;

{ S where S is Subset of T : S_{1}[S] } is Subset-Family of T
from DOMAIN_1:sch 7();

then reconsider IT = { S where S is Subset of T : S_{1}[S] } as Subset-Family of T ;

take IT ; :: thesis: ( IT is open & IT is x -quasi_basis )

IT c= the topology of T

ex V being Subset of T st

( V in IT & V c= S )

let S be Subset of T; :: thesis: ( S is open & x in S implies ex V being Subset of T st

( V in IT & V c= S ) )

assume that

A1: S is open and

A2: x in S ; :: thesis: ex V being Subset of T st

( V in IT & V c= S )

take V = S; :: thesis: ( V in IT & V c= S )

V in the topology of T by A1;

hence V in IT by A2; :: thesis: V c= S

thus V c= S ; :: thesis: verum

set IT = { S where S is Subset of T : S

{ S where S is Subset of T : S

then reconsider IT = { S where S is Subset of T : S

take IT ; :: thesis: ( IT is open & IT is x -quasi_basis )

IT c= the topology of T

proof

hence
IT is open
by TOPS_2:64; :: thesis: IT is x -quasi_basis
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in IT or e in the topology of T )

assume e in IT ; :: thesis: e in the topology of T

then ex S being Subset of T st

( S = e & S in the topology of T & x in S ) ;

hence e in the topology of T ; :: thesis: verum

end;assume e in IT ; :: thesis: e in the topology of T

then ex S being Subset of T st

( S = e & S in the topology of T & x in S ) ;

hence e in the topology of T ; :: thesis: verum

now :: thesis: for e being set st e in IT holds

x in e

hence
x in Intersect IT
by SETFAM_1:43; :: according to YELLOW_8:def 1 :: thesis: for S being Subset of T st S is open & x in S holds x in e

let e be set ; :: thesis: ( e in IT implies x in e )

assume e in IT ; :: thesis: x in e

then ex S being Subset of T st

( S = e & S in the topology of T & x in S ) ;

hence x in e ; :: thesis: verum

end;assume e in IT ; :: thesis: x in e

then ex S being Subset of T st

( S = e & S in the topology of T & x in S ) ;

hence x in e ; :: thesis: verum

ex V being Subset of T st

( V in IT & V c= S )

let S be Subset of T; :: thesis: ( S is open & x in S implies ex V being Subset of T st

( V in IT & V c= S ) )

assume that

A1: S is open and

A2: x in S ; :: thesis: ex V being Subset of T st

( V in IT & V c= S )

take V = S; :: thesis: ( V in IT & V c= S )

V in the topology of T by A1;

hence V in IT by A2; :: thesis: V c= S

thus V c= S ; :: thesis: verum