theorem bagset2: :: FIELD_14:14

for F being Field
for B being non zero bag of the carrier of F
for S1 being non empty finite Subset of F holds
( B divides Bag S1 iff ex S2 being non empty finite Subset of F st
( B = Bag S2 & S2 c= S1 ) )