We will prove topology_on unit_interval unit_interval_topology.

An exact proof term for the current goal is (subspace_topology_is_topology R R_standard_topology unit_interval R_standard_topology_is_topology unit_interval_sub_R).

∎