theorem Th7: :: GROEB_2:7

for X being set
for b1, b2 being bag of X holds
( b2 divides b1 iff lcm (b1,b2) = b1 )