defpred S₁[ set , set ] means for A being Subset of T st A is open holds
( $1 in A iff $2 in A );
consider R being Relation of the carrier of T, the carrier of T such that
A1: for p, q being Element of T holds
( [p,q] in R iff S₁[p,q] ) from RELSET_1:sch 2();
A2: R is_transitive_in the carrier of T

proof

let x, y, z be object ; :: according to RELAT_2:def 8 :: thesis: ( not x in the carrier of T or not y in the carrier of T or not z in the carrier of T or not [x,y] in R or not [y,z] in R or [x,z] in R )
assume that
A3: ( x in the carrier of T & y in the carrier of T & z in the carrier of T ) and
A4: [x,y] in R and
A5: [y,z] in R ; :: thesis: [x,z] in R
reconsider x9 = x, y9 = y, z9 = z as Element of T by A3;
for A being Subset of T st A is open holds
( x9 in A iff z9 in A )

proof

let A be Subset of T; :: thesis: ( A is open implies ( x9 in A iff z9 in A ) )
assume A6: A is open ; :: thesis: ( x9 in A iff z9 in A )
then ( x9 in A iff y9 in A ) by A1, A4;
hence ( x9 in A iff z9 in A ) by A1, A5, A6; :: thesis: verum

end;

hence [x,z] in R by A1; :: thesis: verum

end;

R is_reflexive_in the carrier of T

proof

let x be object ; :: according to RELAT_2:def 1 :: thesis: ( not x in the carrier of T or [x,x] in R )
A7: for A being Subset of T st A is open holds
( x in A iff x in A ) ;
assume x in the carrier of T ; :: thesis: [x,x] in R
hence [x,x] in R by A1, A7; :: thesis: verum

end;

then A8: ( dom R = the carrier of T & field R = the carrier of T ) by ORDERS_1:13;
R is_symmetric_in the carrier of T

proof

let x, y be object ; :: according to RELAT_2:def 3 :: thesis: ( not x in the carrier of T or not y in the carrier of T or not [x,y] in R or [y,x] in R )
assume that
A9: ( x in the carrier of T & y in the carrier of T ) and
A10: [x,y] in R ; :: thesis: [y,x] in R
for A being Subset of T st A is open holds
( y in A iff x in A ) by A1, A9, A10;
hence [y,x] in R by A1, A9; :: thesis: verum

end;

then reconsider R = R as Equivalence_Relation of the carrier of T by A8, A2, PARTFUN1:def 2, RELAT_2:def 11, RELAT_2:def 16;
take R ; :: thesis: for p, q being Point of T holds
( [p,q] in R iff for A being Subset of T st A is open holds
( p in A iff q in A ) )
let p, q be Point of T; :: thesis: ( [p,q] in R iff for A being Subset of T st A is open holds
( p in A iff q in A ) )
thus ( [p,q] in R implies for A being Subset of T st A is open holds
( p in A iff q in A ) ) by A1; :: thesis: ( ( for A being Subset of T st A is open holds
( p in A iff q in A ) ) implies [p,q] in R )
assume for A being Subset of T st A is open holds
( p in A iff q in A ) ; :: thesis: [p,q] in R
hence [p,q] in R by A1; :: thesis: verum