:: deftheorem defines divides ARYTM_3:def 3 :
for k, n being Ordinal holds
( k divides n iff ex a being Ordinal st n = k *^ a );