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 )

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

hence
R1 = R2
by RELAT_1:def 2; :: thesis: verum
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 )

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;thus ( [x,y] in R1 implies [x,y] in R2 ) :: thesis: ( [x,y] in R2 implies [x,y] in R1 )

proof

assume A9:
[x,y] in R2
; :: thesis: [x,y] in R1
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;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

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