let R1, R2 be Equivalence_Relation of the carrier of T; :: thesis: ( ( for p, q being Point of T holds

( [p,q] in R1 iff for A being Subset of T st A is open holds

( p in A iff q in A ) ) ) & ( for p, q being Point of T holds

( [p,q] in R2 iff for A being Subset of T st A is open holds

( p in A iff q in A ) ) ) implies R1 = R2 )

assume that

A11: for p, q being Point of T holds

( [p,q] in R1 iff for A being Subset of T st A is open holds

( p in A iff q in A ) ) and

A12: for p, q being Point of T holds

( [p,q] in R2 iff for A being Subset of T st A is open holds

( p in A iff q in A ) ) ; :: thesis: R1 = R2

let x, y be Point of T; :: according to RELSET_1:def 2 :: thesis: ( ( not [x,y] in R1 or [x,y] in R2 ) & ( not [x,y] in R2 or [x,y] in R1 ) )

( [x,y] in R1 iff for A being Subset of T st A is open holds

( x in A iff y in A ) ) by A11;

hence ( ( not [x,y] in R1 or [x,y] in R2 ) & ( not [x,y] in R2 or [x,y] in R1 ) ) by A12; :: thesis: verum

( [p,q] in R1 iff for A being Subset of T st A is open holds

( p in A iff q in A ) ) ) & ( for p, q being Point of T holds

( [p,q] in R2 iff for A being Subset of T st A is open holds

( p in A iff q in A ) ) ) implies R1 = R2 )

assume that

A11: for p, q being Point of T holds

( [p,q] in R1 iff for A being Subset of T st A is open holds

( p in A iff q in A ) ) and

A12: for p, q being Point of T holds

( [p,q] in R2 iff for A being Subset of T st A is open holds

( p in A iff q in A ) ) ; :: thesis: R1 = R2

let x, y be Point of T; :: according to RELSET_1:def 2 :: thesis: ( ( not [x,y] in R1 or [x,y] in R2 ) & ( not [x,y] in R2 or [x,y] in R1 ) )

( [x,y] in R1 iff for A being Subset of T st A is open holds

( x in A iff y in A ) ) by A11;

hence ( ( not [x,y] in R1 or [x,y] in R2 ) & ( not [x,y] in R2 or [x,y] in R1 ) ) by A12; :: thesis: verum