theorem Th13h: :: FIELD_11:2

for n, m being Ordinal
for b1, b2 being bag of n st support b1 = {m} holds
( b2 divides b1 iff ( b2 = EmptyBag n or ( support b2 = {m} & b2 . m <= b1 . m ) ) )