Let a and y be given.

Assume HaR: a ∈ R.

Assume Hy: y ∈ closed_interval a a.

We will prove y = a.

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

Use reflexivity.

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

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

An exact proof term for the current goal is Hy.

We prove the intermediate claim HyR: y ∈ R.

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

We prove the intermediate claim Hyprop: ¬ (Rlt y a) ∧ ¬ (Rlt a y).

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

We prove the intermediate claim Hnlt_ya: ¬ (Rlt y a).

An exact proof term for the current goal is (andEL (¬ (Rlt y a)) (¬ (Rlt a y)) Hyprop).

We prove the intermediate claim Hnlt_ay: ¬ (Rlt a y).

An exact proof term for the current goal is (andER (¬ (Rlt y a)) (¬ (Rlt a y)) Hyprop).

We prove the intermediate claim Hale: Rle a y.

An exact proof term for the current goal is (RleI a y HaR HyR Hnlt_ya).

We prove the intermediate claim Hya: Rle y a.

An exact proof term for the current goal is (RleI y a HyR HaR Hnlt_ay).

We prove the intermediate claim Haeq: a = y.

An exact proof term for the current goal is (Rle_antisym a y Hale Hya).

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

Use reflexivity.

∎