defpred S_{1}[ 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_{1}[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 )

consider R being Relation of INT,INT such that

A1: for x, y being Element of INT holds

( [x,y] in R iff S

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

hence
( [x,y] in R iff x,y are_congruent_mod m )
; :: thesis: verum
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_{1}[x,y] )
by A1;

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

end;reconsider x = x, y = y as Element of INT by INT_1:def 2;

( [x,y] in R iff S

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