let P1, P2 be Relation of INT; :: thesis: ( ( for x, y being Integer holds

( [x,y] in P1 iff x,y are_congruent_mod m ) ) & ( for x, y being Integer holds

( [x,y] in P2 iff x,y are_congruent_mod m ) ) implies P1 = P2 )

assume that

A2: for x, y being Integer holds

( [x,y] in P1 iff x,y are_congruent_mod m ) and

A3: for x, y being Integer holds

( [x,y] in P2 iff x,y are_congruent_mod m ) ; :: thesis: P1 = P2

A4: for x, y being Integer holds

( [x,y] in P1 iff [x,y] in P2 ) by A2, A3;

thus P1 c= P2 :: according to XBOOLE_0:def 10 :: thesis: P2 c= P1

assume A8: a in P2 ; :: thesis: a in P1

then consider x, y being object such that

A9: a = [x,y] and

A10: ( x in INT & y in INT ) by RELSET_1:2;

reconsider x = x, y = y as Integer by A10;

[x,y] in P1 by A4, A8, A9;

hence a in P1 by A9; :: thesis: verum

( [x,y] in P1 iff x,y are_congruent_mod m ) ) & ( for x, y being Integer holds

( [x,y] in P2 iff x,y are_congruent_mod m ) ) implies P1 = P2 )

assume that

A2: for x, y being Integer holds

( [x,y] in P1 iff x,y are_congruent_mod m ) and

A3: for x, y being Integer holds

( [x,y] in P2 iff x,y are_congruent_mod m ) ; :: thesis: P1 = P2

A4: for x, y being Integer holds

( [x,y] in P1 iff [x,y] in P2 ) by A2, A3;

thus P1 c= P2 :: according to XBOOLE_0:def 10 :: thesis: P2 c= P1

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in P2 or a in P1 )
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in P1 or a in P2 )

assume A5: a in P1 ; :: thesis: a in P2

then consider x, y being object such that

A6: a = [x,y] and

A7: ( x in INT & y in INT ) by RELSET_1:2;

reconsider x = x, y = y as Integer by A7;

[x,y] in P2 by A4, A5, A6;

hence a in P2 by A6; :: thesis: verum

end;assume A5: a in P1 ; :: thesis: a in P2

then consider x, y being object such that

A6: a = [x,y] and

A7: ( x in INT & y in INT ) by RELSET_1:2;

reconsider x = x, y = y as Integer by A7;

[x,y] in P2 by A4, A5, A6;

hence a in P2 by A6; :: thesis: verum

assume A8: a in P2 ; :: thesis: a in P1

then consider x, y being object such that

A9: a = [x,y] and

A10: ( x in INT & y in INT ) by RELSET_1:2;

reconsider x = x, y = y as Integer by A10;

[x,y] in P1 by A4, A8, A9;

hence a in P1 by A9; :: thesis: verum