theorem Th23: :: BAGORDER:26

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 ) & o is_strongly_connected_in Bags n holds
Graded o is admissible