defpred S₁[ set ] means ( $1 in the topology of T & x in $1 );
set IT = { S where S is Subset of T : S₁[S] } ;
{ S where S is Subset of T : S₁[S] } is Subset-Family of T from DOMAIN_1:sch 7();
then reconsider IT = { S where S is Subset of T : S₁[S] } as Subset-Family of T ;
take IT ; :: thesis: ( IT c= the topology of T & x in Intersect IT & ( 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 ) ) )
thus IT c= the topology of T :: thesis: ( x in Intersect IT & ( 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 ) ) )

proof

let e be set ; :: 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;

now

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:58; :: 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, PRE_TOPC:def 5;
hence V in IT by A2; :: thesis: V c= S
thus V c= S ; :: thesis: verum