defpred S_{1}[ 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_{1}[p,q] )
from RELSET_1:sch 2();

A2: R is_transitive_in the carrier of T

R is_symmetric_in the carrier of T

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

( $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

A2: R is_transitive_in the carrier of T

proof

R is_reflexive_in the carrier of T
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 )

end;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

hence
[x,z] in R
by A1; :: thesis: verum
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;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

proof

then A8:
( dom R = the carrier of T & field R = the carrier of T )
by ORDERS_1:13;
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;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

R is_symmetric_in the carrier of T

proof

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;
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;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

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