Let a and b be given.

We will prove topology_on (closed_interval a b) (closed_interval_topology a b).

An exact proof term for the current goal is (subspace_topology_is_topology R R_standard_topology (closed_interval a b) R_standard_topology_is_topology (closed_interval_sub_R a b)).

∎