We will prove topology_on topologists_sine_curve topologists_sine_curve_topology.

An exact proof term for the current goal is (subspace_topology_is_topology EuclidPlane R2_standard_topology topologists_sine_curve EuclidPlane_R2_standard_topology_on topologists_sine_curve_subset_EuclidPlane).

∎