theorem Th6: :: GROEB_3:6

for n being Ordinal
for T being admissible TermOrder of n
for b1, b2, b3, b4 being bag of n st b1 <= b2,T & b3 < b4,T holds
b1 + b3 < b2 + b4,T