Axiom. lub_property
A ⊆ ℝ → ¬A = ∅ → (∃b. b ∈ ℝ ∧ upper_bound b A) → (∃s. s ∈ ℝ ∧ is_sup s A)