defpred S₁[ 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 & S₁[x,y] ) ) from RELSET_1:sch 1();
take G = TopRelStr(# the carrier of T,R, the topology of T #); :: thesis: ( 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 #) ; :: thesis: 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; :: thesis: verum