no goals
α : Type u_1
β : Type ?u.513
γ : Type ?u.516
ι : Type ?u.519
ι' : Type ?u.522
r✝ p q : α → α → Prop
f g : ι → α
s✝ t u : Set α
a b : α
r : α → α → Prop
s : Set (Set α)
h : DirectedOn (fun x x_1 => x ⊆ x_1) s
⊢ Set.Pairwise (⋃₀ s) r ↔ ∀ (a : Set α), a ∈ s → Set.Pairwise a r
rw [sUnion_eq_iUnion, pairwise_iUnion h.directed_val, SetCoe.forall]