:: deftheorem Def1 defines lcm INT_2:def 1 :
for a, b being Integer
for b₃ being Nat holds
( b₃ = a lcm b iff ( a divides b₃ & b divides b₃ & ( for m being Integer st a divides m & b divides m holds
b₃ divides m ) ) );