for o being infinite Ordinal holds not GrLexOrder o is well-ordering