theorem Th3: :: GROEB_3:3

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