for o being Ordinal holds InvLexOrder o is well-ordering