:: deftheorem defines divides INT_1:def 3 :
for i1, i2 being Integer holds
( i1 divides i2 iff ex i3 being Integer st i2 = i1 * i3 );