defpred S₁[ set ] means for p being Element of S st p in $1 holds
for N being net of S st [N,p] in C holds
N is_eventually_in $1;
reconsider X = { V where V is Subset of S : S₁[V] } as Subset-Family of S from DOMAIN_1:sch 7();
take TopStruct(# the carrier of S,X #) ; :: thesis: ( the carrier of TopStruct(# the carrier of S,X #) = the carrier of S & the topology of TopStruct(# the carrier of S,X #) = { V where V is Subset of S : for p being Element of S st p in V holds
for N being net of S st [N,p] in C holds
N is_eventually_in V } )
thus ( the carrier of TopStruct(# the carrier of S,X #) = the carrier of S & the topology of TopStruct(# the carrier of S,X #) = { V where V is Subset of S : for p being Element of S st p in V holds
for N being net of S st [N,p] in C holds
N is_eventually_in V } ) ; :: thesis: verum