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

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

let x, y be object ; :: thesis: ( x in Bags n & y in Bags n & not [x,y] in Graded o implies [b₂,b₁] 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₂,b₁] 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₂,b₁] in Graded o
then A6: TotDegree x9 >= TotDegree y9 by A1, Def7;

per cases ( TotDegree y9 < TotDegree x9 or TotDegree y9 = TotDegree x9 ) by A6, XXREAL_0:1;

suppose TotDegree y9 < TotDegree x9 ; :: thesis: [b₂,b₁] in Graded o

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

end;

suppose A7: TotDegree y9 = TotDegree x9 ; :: thesis: [b₂,b₁] in Graded o

then not [x,y] in o by A1, A5, Def7;
then [y,x] in o by A2, A3, A4;
hence [y,x] in Graded o by A1, A7, Def7; :: thesis: verum

end;

end;

end;

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
[(a + c),(b + c)] in Graded o ) )

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

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

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:3; :: thesis: verum

end;

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

then TotDegree a <> 0 by Th14;
hence [(EmptyBag n),a] in Graded o by A1, A8, Def7; :: thesis: verum

end;

end;

end;

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

let a, b, c be bag of n; :: thesis: ( [a,b] in Graded o implies [(b₁ + b₃),(b₂ + b₃)] in Graded o )
assume A9: [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, A9, Def7;

suppose A10: TotDegree a < TotDegree b ; :: thesis: [(b₁ + b₃),(b₂ + b₃)] 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;

suppose A12: ( 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 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;

end;

end;

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