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
A7: 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
A8: 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 3 :: 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 A7;
hence ( ( not [x,y] in R1 or [x,y] in R2 ) & ( not [x,y] in R2 or [x,y] in R1 ) ) by A8; :: thesis: verum