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: for x, y being Integer holds
( [x,y] in R iff x,y are_congruent_mod m )
let x, y be Integer; :: thesis: ( [x,y] in R iff x,y are_congruent_mod m )
for x, y being Integer holds
( [x,y] in R iff x,y are_congruent_mod m )

proof

let x, y be Integer; :: thesis: ( [x,y] in R iff x,y are_congruent_mod m )
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: verum

end;

hence ( [x,y] in R iff x,y are_congruent_mod m ) ; :: thesis: verum