Let J, le, i and j be given.

Assume HJ: directed_set J le.

Assume HiJ: i ∈ J.

Assume HjJ: j ∈ J.

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

An exact proof term for the current goal is (directed_set_upper_bound_property J le HJ i j HiJ HjJ).

∎