defpred S1[ 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 S1[p,q] ) from 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 ;
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