defpred S1[ set ] means ( T in the topology of T & x in T );
set IT = { S where S is Subset of T : S1[S] } ;
{ S where S is Subset of T : S1[S] } is Subset-Family of T from DOMAIN_1:sch 7();
 then reconsider IT = { S where S is Subset of T : S1[S] } as Subset-Family of T ;
take IT ; :: thesis: ( IT is open & IT is x -quasi_basis )
IT c= the topology of T
proof
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;
hence IT is open by TOPS_2:64; :: thesis: IT is x -quasi_basis
now :: thesis: for e being set st e in IT 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;
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
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