:: deftheorem Def2 defines lcmlat NAT_LAT:def 2 :
for b₁ being BinOp of NAT holds
( b₁ = lcmlat iff for n, m being Nat holds b₁ . (m,n) = m lcm n );