exact ⟨fun b hab ↦ hs hab ha.1, fun b hab ↦ ht hab ha.2⟩
α : Type u_1
inst✝ : BooleanAlgebra α
s t u : Finset α
a✝ : α
hs : IsLowerSet ↑s
ht : IsUpperSet ↑t
a : α
ha : a ∈ s ∧ a ∈ t
⊢ (∀ ⦃b : α⦄, b ≤ a → b ∈ s) ∧ ∀ ⦃b : α⦄, a ≤ b → b ∈ t
no goals