theorem Th19: :: BAGORDER:22

for n being Ordinal holds LexOrder n is admissible