:: deftheorem defines <= TERMORD:def 2 :
for n being Ordinal
for T being TermOrder of n
for b, b9 being bag of n holds
( b <= b9,T iff [b,b9] in T );