let n be Ordinal; :: thesis: for o being TermOrder of n st ( for a, b, c being bag of 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 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 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

let x, y be set ; :: thesis: ( x in Bags n & y in Bags n & not [x,y] in Graded o implies [b₂,b₁] in Graded o )
assume A3: ( x in Bags n & y in Bags n ) ; :: thesis: ( not [x,y] in Graded o implies [b₂,b₁] in Graded o )
reconsider x' = x, y' = y as bag of by A3, POLYNOM1:def 14;
assume A4: not [x,y] in Graded o ; :: thesis: [b₂,b₁] in Graded o
then A5: TotDegree x' >= TotDegree y' by A1, Def9;

per cases ( TotDegree y' < TotDegree x' or TotDegree y' = TotDegree x' ) by A5, XXREAL_0:1;

suppose TotDegree y' < TotDegree x' ; :: thesis: [b₂,b₁] in Graded o

hence [y,x] in Graded o by A1, Def9; :: thesis: verum

end;

suppose A6: TotDegree y' = TotDegree x' ; :: thesis: [b₂,b₁] in Graded o

then not [x,y] in o by A1, A4, Def9;
then [y,x] in o by A2, A3, RELAT_2:def 7;
hence [y,x] in Graded o by A1, A6, Def9; :: thesis: verum

end;

end;

end;

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

now

let a be bag of ; :: thesis: [(EmptyBag n),b₁] in Graded o
A7: TotDegree (EmptyBag n) = 0 by Th16;

per cases ( a = EmptyBag n or a <> EmptyBag n ) ;

suppose a = EmptyBag n ; :: thesis: [(EmptyBag n),b₁] in Graded o

hence [(EmptyBag n),a] in Graded o by ORDERS_1:12; :: thesis: verum

end;

suppose a <> EmptyBag n ; :: thesis: [(EmptyBag n),b₁] in Graded o

then TotDegree a <> 0 by Th16;
then TotDegree (EmptyBag n) < TotDegree a by A7;
hence [(EmptyBag n),a] in Graded o by A1, Def9; :: thesis: verum

end;

end;

end;

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

now

let a, b, c be bag of ; :: thesis: ( [a,b] in Graded o implies [(b₁ + b₃),(b₂ + b₃)] in Graded o )
assume A8: [a,b] in Graded o ; :: thesis: [(b₁ + b₃),(b₂ + b₃)] in Graded o

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

suppose A9: TotDegree a < TotDegree b ; :: thesis: [(b₁ + b₃),(b₂ + b₃)] in Graded o

A10: TotDegree (a + c) = (TotDegree a) + (TotDegree c) by Th14;
TotDegree (b + c) = (TotDegree b) + (TotDegree c) by Th14;
then TotDegree (a + c) < TotDegree (b + c) by A9, A10, XREAL_1:10;
hence [(a + c),(b + c)] in Graded o by A1, Def9; :: thesis: verum

end;

suppose A11: ( TotDegree a = TotDegree b & [a,b] in o ) ; :: thesis: [(b₁ + b₃),(b₂ + b₃)] in Graded o

then TotDegree (a + c) = (TotDegree b) + (TotDegree c) by Th14;
then A12: TotDegree (a + c) = TotDegree (b + c) by Th14;
[(a + c),(b + c)] in o by A1, A11;
hence [(a + c),(b + c)] in Graded o by A1, A12, Def9; :: thesis: verum

end;

end;

end;

hence for a, b, c being bag of st [a,b] in Graded o holds
[(a + c),(b + c)] in Graded o ; :: thesis: verum