:: deftheorem Def4 defines lcm NAT_D:def 4 :
for k, n being natural Number
for b₃ being set holds
( b₃ = k lcm n iff ( k divides b₃ & n divides b₃ & ( for m being Nat st k divides m & n divides m holds
b₃ divides m ) ) );