Let A and l be given.

Assume Hlub: R_lub A l.

We prove the intermediate claim Hcore: l ∈ R ∧ (∀a : set, a ∈ A → a ∈ R → Rle a l).

An exact proof term for the current goal is (andEL (l ∈ R ∧ (∀a : set, a ∈ A → a ∈ R → Rle a l)) (∀u : set, u ∈ R → (∀a : set, a ∈ A → a ∈ R → Rle a u) → Rle l u) Hlub).

An exact proof term for the current goal is (andEL (l ∈ R) (∀a : set, a ∈ A → a ∈ R → Rle a l) Hcore).

∎