no goals
α : Type u_1
β : Type ?u.95088
γ : Type ?u.95091
ι : Sort ?u.95094
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set α
hb : BddAbove s
⊢ ↑(sSup s) = ⨆ (a : α) (_ : a ∈ s), ↑a
rw [coe_sSup' hb, sSup_image]