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