:: deftheorem defines < TERMORD:def 3 :
for n being Ordinal
for T being TermOrder of n
for b, b9 being bag of n holds
( b < b9,T iff ( b <= b9,T & b <> b9 ) );