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);

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

( 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

hence A7:
the InternalRel of (NaivelyOrderedBags n) c= o
by RELAT_1:def 3; :: thesis: o is well-ordering [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;

[(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;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

then A6:
(b1 -' a1) + a1 = b1
by PBOOLE:3;((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;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

[(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

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