theorem Th24: :: BAGORDER:27

for n being Ordinal holds GrLexOrder n is admissible