let n be Ordinal; :: thesis: 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

let o be TermOrder of n; :: thesis: ( ( 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 implies Graded o is admissible )

assume that

A1: for a, b, c being bag of n st [a,b] in o holds

[(a + c),(b + c)] in o and

A2: o is_strongly_connected_in Bags n ; :: thesis: Graded o is admissible

[(a + c),(b + c)] in Graded o ) )

[(a + c),(b + c)] in Graded o

[(a + c),(b + c)] in Graded o ; :: thesis: verum

[(a + c),(b + c)] in o ) & o is_strongly_connected_in Bags n holds

Graded o is admissible

let o be TermOrder of n; :: thesis: ( ( 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 implies Graded o is admissible )

assume that

A1: for a, b, c being bag of n st [a,b] in o holds

[(a + c),(b + c)] in o and

A2: o is_strongly_connected_in Bags n ; :: thesis: Graded o is admissible

now :: thesis: for x, y being object st x in Bags n & y in Bags n & not [x,y] in Graded o holds

[y,x] in Graded o

hence
Graded o is_strongly_connected_in Bags n
; :: according to BAGORDER:def 5 :: thesis: ( ( for a being bag of n holds [(EmptyBag n),a] in Graded o ) & ( for a, b, c being bag of n st [a,b] in Graded o holds [y,x] in Graded o

let x, y be object ; :: thesis: ( x in Bags n & y in Bags n & not [x,y] in Graded o implies [b_{2},b_{1}] in Graded o )

assume that

A3: x in Bags n and

A4: y in Bags n ; :: thesis: ( not [x,y] in Graded o implies [b_{2},b_{1}] in Graded o )

reconsider x9 = x, y9 = y as bag of n by A3, A4;

assume A5: not [x,y] in Graded o ; :: thesis: [b_{2},b_{1}] in Graded o

then A6: TotDegree x9 >= TotDegree y9 by A1, Def7;

end;assume that

A3: x in Bags n and

A4: y in Bags n ; :: thesis: ( not [x,y] in Graded o implies [b

reconsider x9 = x, y9 = y as bag of n by A3, A4;

assume A5: not [x,y] in Graded o ; :: thesis: [b

then A6: TotDegree x9 >= TotDegree y9 by A1, Def7;

[(a + c),(b + c)] in Graded o ) )

now :: thesis: for a being bag of n holds [(EmptyBag n),a] in Graded o

hence
for a being bag of n holds [(EmptyBag n),a] in Graded o
; :: thesis: for a, b, c being bag of n st [a,b] in Graded o holds let a be bag of n; :: thesis: [(EmptyBag n),b_{1}] in Graded o

A8: TotDegree (EmptyBag n) = 0 by Th14;

end;A8: TotDegree (EmptyBag n) = 0 by Th14;

[(a + c),(b + c)] in Graded o

now :: thesis: for a, b, c being bag of n st [a,b] in Graded o holds

[(a + c),(b + c)] in Graded o

hence
for a, b, c being bag of n st [a,b] in Graded o holds [(a + c),(b + c)] in Graded o

let a, b, c be bag of n; :: thesis: ( [a,b] in Graded o implies [(b_{1} + b_{3}),(b_{2} + b_{3})] in Graded o )

assume A9: [a,b] in Graded o ; :: thesis: [(b_{1} + b_{3}),(b_{2} + b_{3})] in Graded o

end;assume A9: [a,b] in Graded o ; :: thesis: [(b

per cases
( TotDegree a < TotDegree b or ( TotDegree a = TotDegree b & [a,b] in o ) )
by A1, A9, Def7;

end;

suppose A10:
TotDegree a < TotDegree b
; :: thesis: [(b_{1} + b_{3}),(b_{2} + b_{3})] in Graded o

A11:
TotDegree (a + c) = (TotDegree a) + (TotDegree c)
by Th12;

TotDegree (b + c) = (TotDegree b) + (TotDegree c) by Th12;

then TotDegree (a + c) < TotDegree (b + c) by A10, A11, XREAL_1:8;

hence [(a + c),(b + c)] in Graded o by A1, Def7; :: thesis: verum

end;TotDegree (b + c) = (TotDegree b) + (TotDegree c) by Th12;

then TotDegree (a + c) < TotDegree (b + c) by A10, A11, XREAL_1:8;

hence [(a + c),(b + c)] in Graded o by A1, Def7; :: thesis: verum

suppose A12:
( TotDegree a = TotDegree b & [a,b] in o )
; :: thesis: [(b_{1} + b_{3}),(b_{2} + b_{3})] in Graded o

then
TotDegree (a + c) = (TotDegree b) + (TotDegree c)
by Th12;

then A13: TotDegree (a + c) = TotDegree (b + c) by Th12;

[(a + c),(b + c)] in o by A1, A12;

hence [(a + c),(b + c)] in Graded o by A1, A13, Def7; :: thesis: verum

end;then A13: TotDegree (a + c) = TotDegree (b + c) by Th12;

[(a + c),(b + c)] in o by A1, A12;

hence [(a + c),(b + c)] in Graded o by A1, A13, Def7; :: thesis: verum

[(a + c),(b + c)] in Graded o ; :: thesis: verum