We will prove topology_on (setprod R R) R2_dictionary_order_topology.

An exact proof term for the current goal is (topology_from_subbasis_is_topology (setprod R R) (open_rays_subbasis (setprod R R)) (open_rays_subbasis_is_subbasis (setprod R R))).

∎