Let J and le be given.

Assume H: directed_set J le.

We will prove directed_set J le.

An exact proof term for the current goal is H.

∎