let n be Ordinal; :: thesis: GrLexOrder n is admissible
A1: for a, b, c being bag of n st [a,b] in LexOrder n holds
[(a + c),(b + c)] in LexOrder n by Def5;
LexOrder n is_strongly_connected_in Bags n by Def5;
hence GrLexOrder n is admissible by A1, Th23; :: thesis: verum