theorem :: BAGORDER:28

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