no goals
α : Type u_1
β : Type ?u.7423
γ : Type ?u.7426
ι : Sort ?u.7429
κ : ι → Sort ?u.7434
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
p : α → Prop
a : α
⊢ IsUpperSet s ↔ ∀ ⦃a : α⦄, a ∈ s → Ici a ⊆ s
simp [IsUpperSet, subset_def, @forall_swap (_ ∈ s)]