let k be Nat; :: thesis: for n, m, r being Integer holds
( k in divisors (n,m,r) iff ( k mod m = r & k divides n ) )
let n, m, r be Integer; :: thesis: ( k in divisors (n,m,r) iff ( k mod m = r & k divides n ) )

hereby :: thesis: ( k mod m = r & k divides n implies k in divisors (n,m,r) )

assume k in divisors (n,m,r) ; :: thesis: ( k mod m = r & k divides n )
then ex i being Nat st
( k = i & i mod m = r & i divides n ) ;
hence ( k mod m = r & k divides n ) ; :: thesis: verum

end;

thus ( k mod m = r & k divides n implies k in divisors (n,m,r) ) ; :: thesis: verum