:: deftheorem defines divisors NUMBER15:def 1 :
for n, m, r being Integer holds divisors (n,m,r) = { k where k is Nat : ( k mod m = r & k divides n ) } ;