:: deftheorem Def9 defines lcmlatplus NAT_LAT:def 9 :
for b₁ being BinOp of NATPLUS holds
( b₁ = lcmlatplus iff for m, n being NatPlus holds b₁ . (m,n) = m lcm n );