:: deftheorem Def2 defines Divisor NAT_6:def 2 :
for n, b₂ being Nat holds
( b₂ is Divisor of n iff b₂ divides n );