Let a, b and x be given.

Assume HaR: a ∈ R.

Assume HbR: b ∈ R.

Assume Hx: x ∈ closed_interval a b.

We will prove Rle a x ∧ Rle x b.

We prove the intermediate claim HCI_def: closed_interval a b = {t ∈ R|¬ (Rlt t a) ∧ ¬ (Rlt b t)}.

Use reflexivity.

We prove the intermediate claim Hx': x ∈ {t ∈ R|¬ (Rlt t a) ∧ ¬ (Rlt b t)}.

rewrite the current goal using HCI_def (from right to left).

An exact proof term for the current goal is Hx.

We prove the intermediate claim HxR: x ∈ R.

An exact proof term for the current goal is (SepE1 R (λt : set ⇒ ¬ (Rlt t a) ∧ ¬ (Rlt b t)) x Hx').

We prove the intermediate claim Hconj: ¬ (Rlt x a) ∧ ¬ (Rlt b x).

An exact proof term for the current goal is (SepE2 R (λt : set ⇒ ¬ (Rlt t a) ∧ ¬ (Rlt b t)) x Hx').

We prove the intermediate claim Hnlt_xa: ¬ (Rlt x a).

An exact proof term for the current goal is (andEL (¬ (Rlt x a)) (¬ (Rlt b x)) Hconj).

We prove the intermediate claim Hnlt_bx: ¬ (Rlt b x).

An exact proof term for the current goal is (andER (¬ (Rlt x a)) (¬ (Rlt b x)) Hconj).

Apply andI to the current goal.

An exact proof term for the current goal is (RleI a x HaR HxR Hnlt_xa).

An exact proof term for the current goal is (RleI x b HxR HbR Hnlt_bx).

∎