defpred S₁[ Element of INT , Element of INT ] means $1,$2 are_congruent_mod m;
consider R being Relation of INT,INT such that
A1: for x, y being Element of INT holds
( [x,y] in R iff S₁[x,y] ) from RELSET_1:sch 2();
take R ; :: thesis:
let x, y be Integer; :: thesis:
for x, y being Integer holds
( [x,y] in R iff x,y are_congruent_mod m )

let x, y be Integer; :: thesis:
reconsider x = x, y = y as Element of INT by INT_1:def 2;
( [x,y] in R iff S₁[x,y] ) by A1;
hence ( [x,y] in R iff x,y are_congruent_mod m ) ; :: thesis:

end;