refactor(set_theory/*): `o.out.r` → `<` (#12468)
We declare a `linear_order` instance on `o.out.α`, for `o : ordinal`, with `<` def-eq to `o.out.r`. This will improve code clarity and will allow us to state theorems about specific ordinals as ordered structures.
