:: deftheorem Def15 defines Multiple NUMBER14:def 15 :
for i, b₂ being Integer holds
( b₂ is Multiple of i iff i divides b₂ );