Definition. is_sup_equi
is_sup s A ↔ upper_bound s A ∧ (∀b. b ∈ ℝ → upper_bound b A → s ≤ b)