let n be 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 )
reconsider n0 = n as Element of NAT by ORDINAL1:def 12;
set IRN = the InternalRel of (NaivelyOrderedBags n);

now :: thesis: for a, b being object st [a,b] in the InternalRel of (NaivelyOrderedBags n) holds
[a,b] in o

let a, b be object ; :: 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
A3: a in dom the InternalRel of (NaivelyOrderedBags n) by A2, XTUPLE_0:def 12;
b in rng the InternalRel of (NaivelyOrderedBags n) by A2, XTUPLE_0:def 13;
then reconsider a1 = a, b1 = b as Element of Bags n by A3, Def11;
A4: a1 divides b1 by A2, Def11;
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 A4, PRE_POLY:def 11;
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 A5, XREAL_0:def 2
.= b1 . i ;
:: thesis: verum

end;

then A6: (b1 -' a1) + a1 = b1 by PBOOLE:3;
[(EmptyBag n),(b1 -' a1)] in o by A1;
then [((EmptyBag n) + a1),((b1 -' a1) + a1)] in o by A1;
hence [a,b] in o by A6, PRE_POLY:53; :: thesis: verum

end;

hence A7: the InternalRel of (NaivelyOrderedBags n) c= o by RELAT_1:def 3; :: thesis: o is well-ordering
set R = product (n0 --> OrderedNAT);
set S = RelStr(# (Bags n),o #);
A8: RelStr(# (Bags n),o #) is quasi_ordered by DICKSON:def 3;
A9: the InternalRel of (product (n0 --> OrderedNAT)) c= the InternalRel of RelStr(# (Bags n),o #) by A7, Th30;
the carrier of (product (n0 --> OrderedNAT)) = the carrier of RelStr(# (Bags n),o #) by Th29;
then A10: RelStr(# (Bags n),o #) \~ is well_founded by A8, A9, DICKSON:49;
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 A10, DICKSON:16;
then A13: o is_well_founded_in field o by A12;
A14: o is connected by A11, A12;
o is well_founded by A13, WELLORD1:3;
hence o is well-ordering by A14; :: thesis: verum