let n be Element of NAT ; :: thesis: for o being TermOrder of n st o is admissible holds
( the InternalRel of (NaivelyOrderedBags n) c= o & o is well-ordering )
let o be TermOrder of n; :: thesis: ( o is admissible implies ( the InternalRel of (NaivelyOrderedBags n) c= o & o is well-ordering ) )
assume A1: o is admissible ; :: thesis: ( the InternalRel of (NaivelyOrderedBags n) c= o & o is well-ordering )
set IRN = the InternalRel of (NaivelyOrderedBags n);

now

let a, b be set ; :: thesis: ( [a,b] in the InternalRel of (NaivelyOrderedBags n) implies [a,b] in o )
assume A2: [a,b] in the InternalRel of (NaivelyOrderedBags n) ; :: thesis: [a,b] in o
( a in dom the InternalRel of (NaivelyOrderedBags n) & b in rng the InternalRel of (NaivelyOrderedBags n) ) by A2, RELAT_1:20;
then reconsider a1 = a, b1 = b as Element of Bags n by Def13;
A3: a1 divides b1 by A2, Def13;
set l = b1 -' a1;

now

let i be set ; :: thesis: ( i in n implies ((b1 -' a1) + a1) . i = b1 . i )
assume i in n ; :: thesis: ((b1 -' a1) + a1) . i = b1 . i
A4: ((b1 -' a1) + a1) . i = ((b1 -' a1) . i) + (a1 . i) by POLYNOM1:def 5
.= ((b1 . i) -' (a1 . i)) + (a1 . i) by POLYNOM1:def 6 ;
a1 . i <= b1 . i by A3, POLYNOM1:def 13;
then (a1 . i) - (a1 . i) <= (b1 . i) - (a1 . i) by XREAL_1:11;
hence ((b1 -' a1) + a1) . i = ((b1 . i) + (- (a1 . i))) + (a1 . i) by A4, XREAL_0:def 2
.= b1 . i ;
:: thesis: verum

end;

then A5: (b1 -' a1) + a1 = b1 by PBOOLE:3;
[(EmptyBag n),(b1 -' a1)] in o by A1, Def7;
then [((EmptyBag n) + a1),((b1 -' a1) + a1)] in o by A1, Def7;
hence [a,b] in o by A5, POLYNOM1:57; :: thesis: verum

end;

hence A6: the InternalRel of (NaivelyOrderedBags n) c= o by RELAT_1:def 3; :: thesis: o is well-ordering
set R = product (n --> OrderedNAT );
set S = RelStr(# (Bags n),o #);
A7: RelStr(# (Bags n),o #) is quasi_ordered by DICKSON:def 3;
A8: the InternalRel of (product (n --> OrderedNAT )) c= the InternalRel of RelStr(# (Bags n),o #) by A6, Th34;
the carrier of (product (n --> OrderedNAT )) = the carrier of RelStr(# (Bags n),o #) by Th33;
then A9: RelStr(# (Bags n),o #) \~ is well_founded by A7, A8, DICKSON:50;

now

o is_strongly_connected_in Bags n by A1, Def7;
then A10: ( o is_reflexive_in Bags n & o is_connected_in Bags n ) by ORDERS_1:92;
A11: field o = Bags n by ORDERS_1:97;
thus o is reflexive ; :: thesis: ( o is transitive & o is antisymmetric & o is connected & o is well_founded )
thus o is transitive ; :: thesis: ( o is antisymmetric & o is connected & o is well_founded )
thus o is antisymmetric ; :: thesis: ( o is connected & o is well_founded )
thus o is connected by A10, A11, RELAT_2:def 14; :: thesis: o is well_founded
RelStr(# (Bags n),o #) is well_founded by A9, DICKSON:17;
then o is_well_founded_in field o by A11, WELLFND1:def 2;
hence o is well_founded by WELLORD1:5; :: thesis: verum

end;

hence o is well-ordering by WELLORD1:def 4; :: thesis: verum