We will prove Hausdorff_space Sorgenfrey_line Sorgenfrey_topology.

An exact proof term for the current goal is R_lower_limit_topology_Hausdorff.

∎