theorem Th13e: :: FIELD_11:1

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