Simplify ordinal.fixpoints_exist proof by using sup_eq_sup theorem.