have b_maj :  ∀ (y : ℝ), y ∈ A → y ≤ b := fun y y_in ↦ (h y_in).2
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
a b : ℝ
A : Set ℝ
hnonvide : ∃ x, x ∈ A
h : A ⊆ Icc a b
⊢ ∃ x ∈ Icc a b, is_sup A x
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
a b : ℝ
A : Set ℝ
hnonvide : ∃ x, x ∈ A
h : A ⊆ Icc a b
b_maj : ∀ y ∈ A, y ≤ b
⊢ ∃ x ∈ Icc a b, is_sup A x