Let U be given.
Assume HU: U ∈ R_ray_topology.
Assume H1U: 1 ∈ U.
We will prove 0 ∈ U.
We prove the intermediate claim HUcases: U = Empty ∨ U = R ∨ ∃a ∈ R, U = {x ∈ R|Rlt x a}.
An exact proof term for the current goal is (SepE2 (𝒫 R) (λU0 : set ⇒ U0 = Empty ∨ U0 = R ∨ ∃a0 ∈ R, U0 = {x ∈ R|Rlt x a0}) U HU).
Apply (HUcases (0 ∈ U)) to the current goal.
Assume HUR: U = Empty ∨ U = R.
Apply (HUR (0 ∈ U)) to the current goal.
Assume HUe: U = Empty.
Apply FalseE to the current goal.
We prove the intermediate claim H1Empty: 1 ∈ Empty.
We will prove 1 ∈ Empty.
rewrite the current goal using HUe (from right to left) at position 2.
An exact proof term for the current goal is H1U.
An exact proof term for the current goal is ((EmptyE 1) H1Empty).
Assume HUeqR: U = R.
rewrite the current goal using HUeqR (from left to right).
An exact proof term for the current goal is real_0.
Assume Hex: ∃a ∈ R, U = {x ∈ R|Rlt x a}.
Apply Hex to the current goal.
Let a be given.
Assume Hapair: a ∈ R ∧ U = {x ∈ R|Rlt x a}.
We prove the intermediate claim HaR: a ∈ R.
An exact proof term for the current goal is (andEL (a ∈ R) (U = {x ∈ R|Rlt x a}) Hapair).
We prove the intermediate claim HUeq: U = {x ∈ R|Rlt x a}.
An exact proof term for the current goal is (andER (a ∈ R) (U = {x ∈ R|Rlt x a}) Hapair).
rewrite the current goal using HUeq (from left to right).
We will prove 0 ∈ {x ∈ R|Rlt x a}.
We prove the intermediate claim H1in: 1 ∈ {x ∈ R|Rlt x a}.
rewrite the current goal using HUeq (from right to left).
An exact proof term for the current goal is H1U.
We prove the intermediate claim H1lt: Rlt 1 a.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ Rlt x0 a) 1 H1in).
We prove the intermediate claim H0lt1: Rlt 0 1.
An exact proof term for the current goal is (RltI 0 1 real_0 real_1 SNoLt_0_1).
We prove the intermediate claim H0lta: Rlt 0 a.
An exact proof term for the current goal is (Rlt_tra 0 1 a H0lt1 H1lt).
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ Rlt x0 a) 0 real_0 H0lta).
∎