no goals
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort ?u.11330
inst✝ : Frame α
s✝ t : Set α
a b : α
s : Set α
⊢ Disjoint a (sSup s) ↔ ∀ (b : α), b ∈ s → Disjoint a b
simpa only [disjoint_comm] using @sSup_disjoint_iff