let R1, R2 be Equivalence_Relation of (Prop Q); :: thesis: ( ( for p, q being Element of Prop Q holds
( [p,q] in R1 iff p <==> q ) ) & ( for p, q being Element of Prop Q holds
( [p,q] in R2 iff p <==> q ) ) implies R1 = R2 )
assume that
A5: for p, q being Element of Prop Q holds
( [p,q] in R1 iff p <==> q ) and
A6: for p, q being Element of Prop Q holds
( [p,q] in R2 iff p <==> q ) ; :: thesis: R1 = R2
A7: for p, q being Element of Prop Q holds
( [p,q] in R1 iff [p,q] in R2 ) by A5, A6;
for x, y being object holds
( [x,y] in R1 iff [x,y] in R2 )

proof

let x, y be object ; :: thesis: ( [x,y] in R1 iff [x,y] in R2 )
thus ( [x,y] in R1 implies [x,y] in R2 ) :: thesis: ( [x,y] in R2 implies [x,y] in R1 )

proof

assume A8: [x,y] in R1 ; :: thesis: [x,y] in R2
then ( x is Element of Prop Q & y is Element of Prop Q ) by ZFMISC_1:87;
hence [x,y] in R2 by A7, A8; :: thesis: verum

end;

assume A9: [x,y] in R2 ; :: thesis: [x,y] in R1
then ( x is Element of Prop Q & y is Element of Prop Q ) by ZFMISC_1:87;
hence [x,y] in R1 by A7, A9; :: thesis: verum

end;

hence R1 = R2 by RELAT_1:def 2; :: thesis: verum