:: deftheorem Def5 defines admissible BAGORDER:def 5 :
for n being Ordinal
for T being TermOrder of n holds
( T is admissible iff ( T is_strongly_connected_in Bags n & ( for a being bag of n holds [(EmptyBag n),a] in T ) & ( for a, b, c being bag of n st [a,b] in T holds
[(a + c),(b + c)] in T ) ) );