Let J and le be given.
Assume HJ: directed_set J le.
We will prove J ≠ Empty.
We prove the intermediate claim Hleft: J ≠ Empty ∧ partial_order_on J le.
An exact proof term for the current goal is (andEL (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 (andEL (J ≠ Empty) (partial_order_on J le) Hleft).
∎