defpred S1[ object , object ] means ex Y being Subset of T st
( Y = {$2} & $1 in Cl Y );
consider R being Relation of the carrier of T such that
A1:
for x, y being object holds
( [x,y] in R iff ( x in the carrier of T & y in the carrier of T & S1[x,y] ) )
from RELSET_1:sch 1();
take G = TopRelStr(# the carrier of T,R, the topology of T #); ( TopStruct(# the carrier of G, the topology of G #) = TopStruct(# the carrier of T, the topology of T #) & ( for x, y being Element of G holds
( x <= y iff ex Y being Subset of T st
( Y = {y} & x in Cl Y ) ) ) )
thus
TopStruct(# the carrier of G, the topology of G #) = TopStruct(# the carrier of T, the topology of T #)
; for x, y being Element of G holds
( x <= y iff ex Y being Subset of T st
( Y = {y} & x in Cl Y ) )
thus
for x, y being Element of G holds
( x <= y iff ex Y being Subset of T st
( Y = {y} & x in Cl Y ) )
by A1; verum