have Sup_maj : upper_bound A (sSup A) := by
  intro x
  apply le_csSup
  exact ⟨b, b_maj⟩
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
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
a b : ℝ
A : Set ℝ
hnonvide : ∃ x, x ∈ A
h : A ⊆ Icc a b
b_maj : ∀ y ∈ A, y ≤ b
Sup_maj : upper_bound A (sSup A)
⊢ ∃ x ∈ Icc a b, is_sup A x