:: deftheorem defines divides PRE_POLY:def 11 :
for X being set
for d, b being bag of X holds
( d divides b iff for k being object holds d . k <= b . k );