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

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:
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 [b2,b1] in Graded o )
assume that
A3: x in Bags n and
A4: y in Bags n ; :: thesis: ( not [x,y] in Graded o implies [b2,b1] in Graded o )
reconsider x9 = x, y9 = y as bag of n by A3, A4;
assume A5: not [x,y] in Graded o ; :: thesis: [b2,b1] in Graded o
then A6: TotDegree x9 >= TotDegree y9 by ;
per cases ( TotDegree y9 < TotDegree x9 or TotDegree y9 = TotDegree x9 ) by ;
suppose A7: TotDegree y9 = TotDegree x9 ; :: thesis: [b2,b1] 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 [(),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 [(),a] in Graded oend;
hence for a being bag of n holds [(),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 [(b1 + b3),(b2 + b3)] in Graded o )
assume A9: [a,b] in Graded o ; :: thesis: [(b1 + b3),(b2 + b3)] 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: [(b1 + b3),(b2 + b3)] in Graded o
A11: TotDegree (a + c) = () + () by Th12;
TotDegree (b + c) = () + () by Th12;
then TotDegree (a + c) < TotDegree (b + c) by ;
hence [(a + c),(b + c)] in Graded o by ; :: thesis: verum
end;
suppose A12: ( TotDegree a = TotDegree b & [a,b] in o ) ; :: thesis: [(b1 + b3),(b2 + b3)] in Graded o
then TotDegree (a + c) = () + () by Th12;
then A13: TotDegree (a + c) = TotDegree (b + c) by Th12;
[(a + c),(b + c)] in o by ;
hence [(a + c),(b + c)] in Graded o by ; :: 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