theorem Th21: :: BAGORDER:24

for n being Ordinal holds InvLexOrder n is admissible