no goals
α : Type u_1
β : Type ?u.165959
γ : Type ?u.165962
ι : Sort ?u.165965
κ : ι → Sort ?u.165970
inst✝¹ : Preorder α
inst✝ : Preorder β
s t : Set α
x : α
⊢ BddAbove ↑(lowerClosure s) ↔ BddAbove s
simp_rw [BddAbove, upperBounds_lowerClosure]