Let a, b, c and d be given.

Assume HaR: a ∈ R.

Assume HbR: b ∈ R.

Assume HcR: c ∈ R.

Assume HdR: d ∈ R.

Set I to be the term closed_interval a b.

Set Ti to be the term closed_interval_topology a b.

Set C to be the term closed_interval c d.

We will prove closed_in I Ti (C ∩ I).

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.

We prove the intermediate claim HISubR: I ⊆ R.

An exact proof term for the current goal is (closed_interval_sub_R a b).

We prove the intermediate claim HCclosed: closed_in R R_standard_topology C.

An exact proof term for the current goal is (closed_interval_closed_in_R_standard_topology c d HcR HdR).

Apply (iffER (closed_in I Ti (C ∩ I)) (∃D : set, closed_in R R_standard_topology D ∧ (C ∩ I) = D ∩ I) (closed_in_subspace_iff_intersection R R_standard_topology I (C ∩ I) HT HISubR)) to the current goal.

We use C to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HCclosed.

Use reflexivity.

∎