theorem Th22: :: BAGORDER:25

for o being Ordinal holds InvLexOrder o is well-ordering