Definition. upper_bound_equi
upper_bound b A ↔ ∀x. x ∈ A → x ≤ b