:: deftheorem Def10 defines BlockOrder BAGORDER:def 10 :
for i, n being Nat
for o1 being TermOrder of (i + 1)
for o2 being TermOrder of (n -' (i + 1))
for b₅ being TermOrder of n holds
( b₅ = BlockOrder (i,n,o1,o2) iff for p, q being bag of n holds
( [p,q] in b₅ iff ( ( (0,(i + 1)) -cut p <> (0,(i + 1)) -cut q & [((0,(i + 1)) -cut p),((0,(i + 1)) -cut q)] in o1 ) or ( (0,(i + 1)) -cut p = (0,(i + 1)) -cut q & [(((i + 1),n) -cut p),(((i + 1),n) -cut q)] in o2 ) ) ) );