defpred S₁[ set , set ] 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 set 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 ) ) :: thesis: verum

proof

let x, y be Element of G; :: thesis: ( x <= y iff ex Y being Subset of T st
( Y = {y} & x in Cl Y ) )

hereby :: thesis: ( ex Y being Subset of T st
( Y = {y} & x in Cl Y ) implies x <= y )

assume x <= y ; :: thesis: ex Y being Subset of T st
( Y = {y} & x in Cl Y )
then [x,y] in R by ORDERS_2:def 9;
hence ex Y being Subset of T st
( Y = {y} & x in Cl Y ) by A1; :: thesis: verum

end;

given Y being Subset of T such that A2: ( Y = {y} & x in Cl Y ) ; :: thesis: x <= y
[x,y] in R by A1, A2;
hence x <= y by ORDERS_2:def 9; :: thesis: verum

end;