rintro _ ⟨i, hi, rfl⟩ _ ⟨j, hj, rfl⟩
α : Type u_1
s : Set α
ι : Type u_2
inst✝ : LE ι
v : ι → Set α
a : Set ι
hs : s.Finite
ha : DirectedOn (fun x x_1 => x ≤ x_1) a
hne : a.Nonempty
hv : ∀ ⦃i j : ι⦄, i ≤ j → v i ⊆ v j
⊢ DirectedOn (fun x x_1 => x ⊆ x_1) (v '' a)
case intro.intro.intro.intro
α : Type u_1
s : Set α
ι : Type u_2
inst✝ : LE ι
v : ι → Set α
a : Set ι
hs : s.Finite
ha : DirectedOn (fun x x_1 => x ≤ x_1) a
hne : a.Nonempty
hv : ∀ ⦃i j : ι⦄, i ≤ j → v i ⊆ v j
i : ι
hi : i ∈ a
j : ι
hj : j ∈ a
⊢ ∃ z ∈ v '' a, (fun x x_1 => x ⊆ x_1) (v i) z ∧ (fun x x_1 => x ⊆ x_1) (v j) z