theorem Th26: :: BAGORDER:29

for n being Ordinal holds GrInvLexOrder n is admissible