for o1, o2 being Ordinal
for b1, c1 being Element of Bags o1
for b2, c2 being Element of Bags o2 st b1 +^ b2 = c1 +^ c2 holds
( b1 = c1 & b2 = c2 )