Let a, b and x be given.

Assume HaR: a ∈ R.

Assume HbR: b ∈ R.

Assume HxR: x ∈ R.

Assume Hax: Rle a x.

Assume Hxb: Rle x b.

We will prove x ∈ closed_interval a b.

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

Use reflexivity.

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

Apply (SepI R (λt : set ⇒ ¬ (Rlt t a) ∧ ¬ (Rlt b t)) x HxR) to the current goal.

Apply andI to the current goal.

An exact proof term for the current goal is (RleE_nlt a x Hax).

An exact proof term for the current goal is (RleE_nlt x b Hxb).

∎