Assume Hnltxa: ¬ (Rlt x a).

Apply (xm (Rlt b x)) to the current goal.

Assume Hltbx: Rlt b x.

Apply orIR to the current goal.

An exact proof term for the current goal is Hltbx.

Assume Hnltbx: ¬ (Rlt b x).

Apply FalseE to the current goal.

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 Hxin: x ∈ closed_interval a b.

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.

An exact proof term for the current goal is (andI (¬ (Rlt x a)) (¬ (Rlt b x)) Hnltxa Hnltbx).

An exact proof term for the current goal is (Hnot Hxin).