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

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