:: deftheorem defines multiples GROEB_1:def 2 :
for n being Ordinal
for S being Subset of (Bags n) holds multiples S = { b where b is Element of Bags n : ex b9 being bag of n st
( b9 in S & b9 divides b ) } ;