no goals
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝³ : Preorder α
inst✝² : Preorder β
s t : Set α
a b : α
inst✝¹ : PartialOrder γ
inst✝ : OrderTop γ
⊢ upperBounds univ = {⊤}
rw [isGreatest_univ.upperBounds_eq, Ici_top]