We will prove topology_on R (order_topology R).

rewrite the current goal using standard_topology_is_order_topology (from left to right).

An exact proof term for the current goal is R_standard_topology_is_topology.

∎