Let J, le and i be given.

Assume HJ: directed_set J le.

Assume HiJ: i ∈ J.

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

We prove the intermediate claim Hexk: ∃k : set, k ∈ J ∧ (i,k) ∈ le ∧ (i,k) ∈ le.

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

Apply Hexk to the current goal.

Let k be given.

Assume Hk.

We use k to witness the existential quantifier.

An exact proof term for the current goal is (andEL (k ∈ J ∧ (i,k) ∈ le) ((i,k) ∈ le) Hk).

∎