Assume HH: Hausdorff_space R R_ray_topology.
We will prove False.
We prove the intermediate claim Hsep: ∀x1 x2 : set, x1 ∈ R → x2 ∈ R → x1 ≠ x2 → ∃U V : set, U ∈ R_ray_topology ∧ V ∈ R_ray_topology ∧ x1 ∈ U ∧ x2 ∈ V ∧ U ∩ V = Empty.
An exact proof term for the current goal is (andER (topology_on R R_ray_topology) (∀x1 x2 : set, x1 ∈ R → x2 ∈ R → x1 ≠ x2 → ∃U V : set, U ∈ R_ray_topology ∧ V ∈ R_ray_topology ∧ x1 ∈ U ∧ x2 ∈ V ∧ U ∩ V = Empty) HH).
We prove the intermediate claim H01ne: 0 ≠ 1.
Assume H01eq: 0 = 1.
We prove the intermediate claim H00lt: 0 < 0.
rewrite the current goal using H01eq (from left to right) at position 2.
An exact proof term for the current goal is SNoLt_0_1.
An exact proof term for the current goal is ((SNoLt_irref 0) H00lt).
We prove the intermediate claim HUVex: ∃U V : set, U ∈ R_ray_topology ∧ V ∈ R_ray_topology ∧ 0 ∈ U ∧ 1 ∈ V ∧ U ∩ V = Empty.
An exact proof term for the current goal is (Hsep 0 1 real_0 real_1 H01ne).
Apply HUVex to the current goal.
Let U be given.
Assume HVex: ∃V : set, U ∈ R_ray_topology ∧ V ∈ R_ray_topology ∧ 0 ∈ U ∧ 1 ∈ V ∧ U ∩ V = Empty.
Apply HVex to the current goal.
Let V be given.
Assume HUV.
We prove the intermediate claim HUVleft: (((U ∈ R_ray_topology ∧ V ∈ R_ray_topology) ∧ 0 ∈ U) ∧ 1 ∈ V).
An exact proof term for the current goal is (andEL (((U ∈ R_ray_topology ∧ V ∈ R_ray_topology) ∧ 0 ∈ U) ∧ 1 ∈ V) (U ∩ V = Empty) HUV).
We prove the intermediate claim HUVempty: U ∩ V = Empty.
An exact proof term for the current goal is (andER (((U ∈ R_ray_topology ∧ V ∈ R_ray_topology) ∧ 0 ∈ U) ∧ 1 ∈ V) (U ∩ V = Empty) HUV).
We prove the intermediate claim HUVleft2: ((U ∈ R_ray_topology ∧ V ∈ R_ray_topology) ∧ 0 ∈ U).
An exact proof term for the current goal is (andEL ((U ∈ R_ray_topology ∧ V ∈ R_ray_topology) ∧ 0 ∈ U) (1 ∈ V) HUVleft).
We prove the intermediate claim H1V: 1 ∈ V.
An exact proof term for the current goal is (andER ((U ∈ R_ray_topology ∧ V ∈ R_ray_topology) ∧ 0 ∈ U) (1 ∈ V) HUVleft).
We prove the intermediate claim HUVleft3: (U ∈ R_ray_topology ∧ V ∈ R_ray_topology).
An exact proof term for the current goal is (andEL (U ∈ R_ray_topology ∧ V ∈ R_ray_topology) (0 ∈ U) HUVleft2).
We prove the intermediate claim H0U: 0 ∈ U.
An exact proof term for the current goal is (andER (U ∈ R_ray_topology ∧ V ∈ R_ray_topology) (0 ∈ U) HUVleft2).
We prove the intermediate claim HU: U ∈ R_ray_topology.
An exact proof term for the current goal is (andEL (U ∈ R_ray_topology) (V ∈ R_ray_topology) HUVleft3).
We prove the intermediate claim HV: V ∈ R_ray_topology.
An exact proof term for the current goal is (andER (U ∈ R_ray_topology) (V ∈ R_ray_topology) HUVleft3).
We prove the intermediate claim H0V: 0 ∈ V.
An exact proof term for the current goal is (ray_topology_contains_0_if_contains_1 V HV H1V).
We prove the intermediate claim H0UV: 0 ∈ U ∩ V.
An exact proof term for the current goal is (binintersectI U V 0 H0U H0V).
We prove the intermediate claim H0Empty: 0 ∈ Empty.
We will prove 0 ∈ Empty.
rewrite the current goal using HUVempty (from right to left) at position 2.
An exact proof term for the current goal is H0UV.
An exact proof term for the current goal is (EmptyE 0 H0Empty).
∎