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

proof

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;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in P2 or a in 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