Let a and b be given.

Let x be given.

Assume Hx: x ∈ closed_interval a b.

We will prove x ∈ R.

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.

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

∎