for n being Ordinal
for T being TermOrder of n
for b being bag of n holds b <= b,T by Lm2;