Let J and le be given.

We will prove ∀i j : set, i ∈ J → j ∈ J → ∃k : set, k ∈ J ∧ (i,k) ∈ le ∧ (j,k) ∈ le.

Let i and j be given.

Assume HiJ: i ∈ J.

Assume HjJ: j ∈ J.

We prove the intermediate claim Hdir: ∀a b : set, a ∈ J → b ∈ J → ∃c : set, c ∈ J ∧ (a,c) ∈ le ∧ (b,c) ∈ le.

An exact proof term for the current goal is (andER (J ≠ Empty ∧ partial_order_on J le) (∀a b : set, a ∈ J → b ∈ J → ∃c : set, c ∈ J ∧ (a,c) ∈ le ∧ (b,c) ∈ le) HJ).

An exact proof term for the current goal is (Hdir i j HiJ HjJ).

∎