Let A, l1 and l2 be given.
Assume H1: R_lub A l1.
Assume H2: R_lub A l2.
We prove the intermediate claim H1core: l1 ∈ R ∧ ∀a : set, a ∈ A → a ∈ R → Rle a l1.
An exact proof term for the current goal is (andEL (l1 ∈ R ∧ ∀a : set, a ∈ A → a ∈ R → Rle a l1) (∀u : set, u ∈ R → (∀a : set, a ∈ A → a ∈ R → Rle a u) → Rle l1 u) H1).
We prove the intermediate claim H1min: ∀u : set, u ∈ R → (∀a : set, a ∈ A → a ∈ R → Rle a u) → Rle l1 u.
An exact proof term for the current goal is (andER (l1 ∈ R ∧ ∀a : set, a ∈ A → a ∈ R → Rle a l1) (∀u : set, u ∈ R → (∀a : set, a ∈ A → a ∈ R → Rle a u) → Rle l1 u) H1).
We prove the intermediate claim H1R: l1 ∈ R.
An exact proof term for the current goal is (andEL (l1 ∈ R) (∀a : set, a ∈ A → a ∈ R → Rle a l1) H1core).
We prove the intermediate claim H1ub: ∀a : set, a ∈ A → a ∈ R → Rle a l1.
An exact proof term for the current goal is (andER (l1 ∈ R) (∀a : set, a ∈ A → a ∈ R → Rle a l1) H1core).
We prove the intermediate claim H2core: l2 ∈ R ∧ ∀a : set, a ∈ A → a ∈ R → Rle a l2.
An exact proof term for the current goal is (andEL (l2 ∈ R ∧ ∀a : set, a ∈ A → a ∈ R → Rle a l2) (∀u : set, u ∈ R → (∀a : set, a ∈ A → a ∈ R → Rle a u) → Rle l2 u) H2).
We prove the intermediate claim H2min: ∀u : set, u ∈ R → (∀a : set, a ∈ A → a ∈ R → Rle a u) → Rle l2 u.
An exact proof term for the current goal is (andER (l2 ∈ R ∧ ∀a : set, a ∈ A → a ∈ R → Rle a l2) (∀u : set, u ∈ R → (∀a : set, a ∈ A → a ∈ R → Rle a u) → Rle l2 u) H2).
We prove the intermediate claim H2R: l2 ∈ R.
An exact proof term for the current goal is (andEL (l2 ∈ R) (∀a : set, a ∈ A → a ∈ R → Rle a l2) H2core).
We prove the intermediate claim H2ub: ∀a : set, a ∈ A → a ∈ R → Rle a l2.
An exact proof term for the current goal is (andER (l2 ∈ R) (∀a : set, a ∈ A → a ∈ R → Rle a l2) H2core).
We prove the intermediate claim Hle12: Rle l1 l2.
An exact proof term for the current goal is (H1min l2 H2R H2ub).
We prove the intermediate claim Hle21: Rle l2 l1.
An exact proof term for the current goal is (H2min l1 H1R H1ub).
An exact proof term for the current goal is (Rle_antisym l1 l2 Hle12 Hle21).
∎