:: deftheorem defines Divides GAUSSINT:def 18 :
for a, b being G_INTEG holds
( a Divides b iff ex c being G_INTEG st b = a * c );