no goals
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort ?u.10538
inst✝ : Frame α
s✝ t : Set α
a b : α
s : Set α
⊢ Disjoint (sSup s) a ↔ ∀ (b : α), b ∈ s → Disjoint b a
simp only [disjoint_iff, sSup_inf_eq, iSup_eq_bot]