let n be Nat; :: thesis: for o being TermOrder of n st o is admissible holds
( the InternalRel of c= o & o is well-ordering )

let o be TermOrder of n; :: thesis: ( o is admissible implies ( the InternalRel of c= o & o is well-ordering ) )
assume A1: o is admissible ; :: thesis: ( the InternalRel of c= o & o is well-ordering )
reconsider n0 = n as Element of NAT by ORDINAL1:def 12;
set IRN = the InternalRel of ;
now :: thesis: for a, b being object st [a,b] in the InternalRel of holds
[a,b] in o
let a, b be object ; :: thesis: ( [a,b] in the InternalRel of implies [a,b] in o )
assume A2: [a,b] in the InternalRel of ; :: thesis: [a,b] in o
A3: a in dom the InternalRel of by ;
b in rng the InternalRel of by ;
then reconsider a1 = a, b1 = b as Element of Bags n by ;
A4: a1 divides b1 by ;
set l = b1 -' a1;
now :: thesis: for i being object st i in n holds
((b1 -' a1) + a1) . i = b1 . i
let i be object ; :: thesis: ( i in n implies ((b1 -' a1) + a1) . i = b1 . i )
assume i in n ; :: thesis: ((b1 -' a1) + a1) . i = b1 . i
A5: ((b1 -' a1) + a1) . i = ((b1 -' a1) . i) + (a1 . i) by PRE_POLY:def 5
.= ((b1 . i) -' (a1 . i)) + (a1 . i) by PRE_POLY:def 6 ;
a1 . i <= b1 . i by ;
then (a1 . i) - (a1 . i) <= (b1 . i) - (a1 . i) by XREAL_1:9;
hence ((b1 -' a1) + a1) . i = ((b1 . i) + (- (a1 . i))) + (a1 . i) by
.= b1 . i ;
:: thesis: verum
end;
then A6: (b1 -' a1) + a1 = b1 by PBOOLE:3;
[(),(b1 -' a1)] in o by A1;
then [(() + a1),((b1 -' a1) + a1)] in o by A1;
hence [a,b] in o by ; :: thesis: verum
end;
hence A7: the InternalRel of c= o by RELAT_1:def 3; :: thesis:
set R = product ();
set S = RelStr(# (Bags n),o #);
A8: RelStr(# (Bags n),o #) is quasi_ordered by DICKSON:def 3;
A9: the InternalRel of (product ()) c= the InternalRel of RelStr(# (Bags n),o #) by ;
the carrier of (product ()) = the carrier of RelStr(# (Bags n),o #) by Th29;
then A10: RelStr(# (Bags n),o #) \~ is well_founded by ;
o is_strongly_connected_in Bags n by A1;
then A11: o is_connected_in Bags n ;
A12: field o = Bags n by ORDERS_1:12;
RelStr(# (Bags n),o #) is well_founded by ;
then A13: o is_well_founded_in field o by A12;
A14: o is connected by ;
o is well_founded by ;
hence o is well-ordering by A14; :: thesis: verum