for n being Ordinal
for T being admissible TermOrder of n
for b being bag of n holds EmptyBag n <= b,T by BAGORDER:def 5;