:: deftheorem Def2 defines lcm GROEB_2:def 2 :
for X being set
for b1, b2, b₄ being bag of X holds
( b₄ = lcm (b1,b2) iff for k being object holds b₄ . k = max ((b1 . k),(b2 . k)) );