for o being Ordinal holds GrInvLexOrder o is well-ordering