:: deftheorem defines GrInvLexOrder BAGORDER:def 9 :
for n being Ordinal holds GrInvLexOrder n = Graded (InvLexOrder n);