:: deftheorem Def6 defines InvLexOrder BAGORDER:def 6 :
for n being Ordinal
for b₂ being TermOrder of n holds
( b₂ = InvLexOrder n iff for p, q being bag of n holds
( [p,q] in b₂ iff ( p = q or ex i being Ordinal st
( i in n & p . i < q . i & ( for k being Ordinal st i in k & k in n holds
p . k = q . k ) ) ) ) );