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

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