for o1, o2 being Ordinal
for a1, b1 being Element of Bags o1
for a2, b2 being Element of Bags o2 holds
( a1 +^ a2 < b1 +^ b2 iff ( a1 < b1 or ( a1 = b1 & a2 < b2 ) ) )