Let a and b be given.
Assume HaR: a ∈ R.
Assume HbR: b ∈ R.
We will prove closed_in R R_standard_topology (closed_interval a b).
We prove the intermediate claim HT: topology_on R R_standard_topology.
An exact proof term for the current goal is R_standard_topology_is_topology.
Set U to be the term {x ∈ R|Rlt x a}.
Set V to be the term {x ∈ R|Rlt b x}.
We prove the intermediate claim HUopen: U ∈ R_standard_topology.
An exact proof term for the current goal is (open_left_ray_in_R_standard_topology a HaR).
We prove the intermediate claim HVopen: V ∈ R_standard_topology.
An exact proof term for the current goal is (open_ray_in_R_standard_topology b HbR).
We prove the intermediate claim HUVopen: (U ∪ V) ∈ R_standard_topology.
An exact proof term for the current goal is (binunion_in_R_standard_topology U V HUopen HVopen).
We prove the intermediate claim Heq: closed_interval a b = R ∖ (U ∪ V).
Apply set_ext to the current goal.
Let x be given.
Assume HxI: x ∈ closed_interval a b.
We will prove x ∈ R ∖ (U ∪ V).
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 HxI).
We prove the intermediate claim Hxprop: ¬ (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 HxI).
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)) Hxprop).
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)) Hxprop).
Apply setminusI to the current goal.
An exact proof term for the current goal is HxR.
Assume HxUV: x ∈ (U ∪ V).
Apply (binunionE U V x HxUV) to the current goal.
Assume HxU: x ∈ U.
We prove the intermediate claim Hlt: Rlt x a.
An exact proof term for the current goal is (SepE2 R (λt : set ⇒ Rlt t a) x HxU).
An exact proof term for the current goal is (Hnlt_xa Hlt).
Assume HxV: x ∈ V.
We prove the intermediate claim Hlt: Rlt b x.
An exact proof term for the current goal is (SepE2 R (λt : set ⇒ Rlt b t) x HxV).
An exact proof term for the current goal is (Hnlt_bx Hlt).
Let x be given.
Assume Hx: x ∈ R ∖ (U ∪ V).
We will prove x ∈ closed_interval a b.
Apply (setminusE R (U ∪ V) x Hx) to the current goal.
Assume HxR: x ∈ R.
Assume Hxnot: x ∉ (U ∪ V).
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.
Assume Hlt: Rlt x a.
We will prove False.
Apply Hxnot to the current goal.
Apply (binunionI1 U V x) to the current goal.
An exact proof term for the current goal is (SepI R (λt : set ⇒ Rlt t a) x HxR Hlt).
Assume Hlt: Rlt b x.
We will prove False.
Apply Hxnot to the current goal.
Apply (binunionI2 U V x) to the current goal.
An exact proof term for the current goal is (SepI R (λt : set ⇒ Rlt b t) x HxR Hlt).
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is (closed_of_open_complement R R_standard_topology (U ∪ V) HT HUVopen).
∎