theorem bagset1: :: FIELD_14:13

for F being Field
for S1, S2 being non empty finite Subset of F holds
( Bag S1 divides Bag S2 iff S1 c= S2 )