:: deftheorem Def7 defines Graded BAGORDER:def 7 :
for n being Ordinal
for o being TermOrder of n st ( for a, b, c being bag of n st [a,b] in o holds
[(a + c),(b + c)] in o ) holds
for b₃ being TermOrder of n holds
( b₃ = Graded o iff for a, b being bag of n holds
( [a,b] in b₃ iff ( TotDegree a < TotDegree b or ( TotDegree a = TotDegree b & [a,b] in o ) ) ) );