defpred S1[ 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 S1[x,y] )
from RELSET_1:sch 2();
take
R
; for x, y being Integer holds
( [x,y] in R iff x,y are_congruent_mod m )
let x, y be Integer; ( [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 )
hence
( [x,y] in R iff x,y are_congruent_mod m )
; verum