Let x1 and x2 be given.

Assume Hx1X: x1 ∈ X.

Assume Hx2X: x2 ∈ X.

Assume Hne: x1 ≠ x2.

We will prove ∃U V : set, U ∈ order_topology X ∧ V ∈ order_topology X ∧ x1 ∈ U ∧ x2 ∈ V ∧ U ∩ V = Empty.

Apply (order_rel_trichotomy_or_impred X x1 x2 Hso Hx1X Hx2X (∃U V : set, U ∈ order_topology X ∧ V ∈ order_topology X ∧ x1 ∈ U ∧ x2 ∈ V ∧ U ∩ V = Empty)) to the current goal.

Assume H12: order_rel X x1 x2.

Set I to be the term order_interval X x1 x2.

Apply (xm (I = Empty)) to the current goal.

Assume HIEmpty: I = Empty.

Set U to be the term open_ray_lower X x2.

Set V to be the term open_ray_upper X x1.

We use U to witness the existential quantifier.

We use V to witness the existential quantifier.

We will prove U ∈ order_topology X ∧ V ∈ order_topology X ∧ x1 ∈ U ∧ x2 ∈ V ∧ U ∩ V = Empty.

Apply andI to the current goal.

We prove the intermediate claim HUsub: U ∈ open_rays_subbasis X.

An exact proof term for the current goal is (open_ray_lower_in_open_rays_subbasis X x2 Hx2X).

An exact proof term for the current goal is ((open_rays_subbasis_sub_order_topology X Hso) U HUsub).

We prove the intermediate claim HVsub: V ∈ open_rays_subbasis X.

An exact proof term for the current goal is (open_ray_upper_in_open_rays_subbasis X x1 Hx1X).

An exact proof term for the current goal is ((open_rays_subbasis_sub_order_topology X Hso) V HVsub).

We will prove x1 ∈ U.

An exact proof term for the current goal is (SepI X (λt : set ⇒ order_rel X t x2) x1 Hx1X H12).

We will prove x2 ∈ V.

An exact proof term for the current goal is (SepI X (λt : set ⇒ order_rel X x1 t) x2 Hx2X H12).

We will prove U ∩ V = Empty.

Apply set_ext to the current goal.

Let y be given.

Assume Hy: y ∈ U ∩ V.

We will prove y ∈ Empty.

We prove the intermediate claim HyU: y ∈ U.

An exact proof term for the current goal is (binintersectE1 U V y Hy).

We prove the intermediate claim HyV: y ∈ V.

An exact proof term for the current goal is (binintersectE2 U V y Hy).

We prove the intermediate claim HyX: y ∈ X.

An exact proof term for the current goal is (SepE1 X (λt : set ⇒ order_rel X t x2) y HyU).

We prove the intermediate claim Hylt2: order_rel X y x2.

An exact proof term for the current goal is (SepE2 X (λt : set ⇒ order_rel X t x2) y HyU).

We prove the intermediate claim H1lty: order_rel X x1 y.

An exact proof term for the current goal is (SepE2 X (λt : set ⇒ order_rel X x1 t) y HyV).

We prove the intermediate claim HyI: y ∈ I.

An exact proof term for the current goal is (SepI X (λt : set ⇒ order_rel X x1 t ∧ order_rel X t x2) y HyX (andI (order_rel X x1 y) (order_rel X y x2) H1lty Hylt2)).

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

An exact proof term for the current goal is HyI.

Let y be given.

Assume Hy: y ∈ Empty.

We will prove y ∈ U ∩ V.

Apply FalseE to the current goal.

An exact proof term for the current goal is (EmptyE y Hy).

Assume HInon: ¬ (I = Empty).

We prove the intermediate claim HIne: I ≠ Empty.

Assume HIeq: I = Empty.

An exact proof term for the current goal is (HInon HIeq).

Apply (nonempty_has_element I HIne) to the current goal.

Let c be given.

Assume HcI: c ∈ I.

Set U to be the term open_ray_lower X c.

Set V to be the term open_ray_upper X c.

We use U to witness the existential quantifier.

We use V to witness the existential quantifier.

We will prove U ∈ order_topology X ∧ V ∈ order_topology X ∧ x1 ∈ U ∧ x2 ∈ V ∧ U ∩ V = Empty.

We prove the intermediate claim HcX: c ∈ X.

An exact proof term for the current goal is (SepE1 X (λt : set ⇒ order_rel X x1 t ∧ order_rel X t x2) c HcI).

We prove the intermediate claim HcProp: order_rel X x1 c ∧ order_rel X c x2.

An exact proof term for the current goal is (SepE2 X (λt : set ⇒ order_rel X x1 t ∧ order_rel X t x2) c HcI).

We prove the intermediate claim Hx1c: order_rel X x1 c.

An exact proof term for the current goal is (andEL (order_rel X x1 c) (order_rel X c x2) HcProp).

We prove the intermediate claim Hcx2: order_rel X c x2.

An exact proof term for the current goal is (andER (order_rel X x1 c) (order_rel X c x2) HcProp).

Apply andI to the current goal.

We prove the intermediate claim HUsub: U ∈ open_rays_subbasis X.

An exact proof term for the current goal is (open_ray_lower_in_open_rays_subbasis X c HcX).

An exact proof term for the current goal is ((open_rays_subbasis_sub_order_topology X Hso) U HUsub).

We prove the intermediate claim HVsub: V ∈ open_rays_subbasis X.

An exact proof term for the current goal is (open_ray_upper_in_open_rays_subbasis X c HcX).

An exact proof term for the current goal is ((open_rays_subbasis_sub_order_topology X Hso) V HVsub).

We will prove x1 ∈ U.

An exact proof term for the current goal is (SepI X (λt : set ⇒ order_rel X t c) x1 Hx1X Hx1c).

We will prove x2 ∈ V.

An exact proof term for the current goal is (SepI X (λt : set ⇒ order_rel X c t) x2 Hx2X Hcx2).

We will prove U ∩ V = Empty.

Apply set_ext to the current goal.

Let y be given.

Assume Hy: y ∈ U ∩ V.

We will prove y ∈ Empty.

We prove the intermediate claim HyU: y ∈ U.

An exact proof term for the current goal is (binintersectE1 U V y Hy).

We prove the intermediate claim HyV: y ∈ V.

An exact proof term for the current goal is (binintersectE2 U V y Hy).

We prove the intermediate claim HyX: y ∈ X.

An exact proof term for the current goal is (SepE1 X (λt : set ⇒ order_rel X t c) y HyU).

We prove the intermediate claim Hyc: order_rel X y c.

An exact proof term for the current goal is (SepE2 X (λt : set ⇒ order_rel X t c) y HyU).

We prove the intermediate claim Hcy: order_rel X c y.

An exact proof term for the current goal is (SepE2 X (λt : set ⇒ order_rel X c t) y HyV).

We prove the intermediate claim Hyy: order_rel X y y.

An exact proof term for the current goal is (order_rel_trans X y c y Hso HyX HcX HyX Hyc Hcy).

Apply FalseE to the current goal.

An exact proof term for the current goal is (order_rel_irref X y Hyy).

Let y be given.

Assume Hy: y ∈ Empty.

We will prove y ∈ U ∩ V.

Apply FalseE to the current goal.

An exact proof term for the current goal is (EmptyE y Hy).

Assume Heq: x1 = x2.

An exact proof term for the current goal is (FalseE (Hne Heq) (∃U V : set, U ∈ order_topology X ∧ V ∈ order_topology X ∧ x1 ∈ U ∧ x2 ∈ V ∧ U ∩ V = Empty)).

Assume H21: order_rel X x2 x1.

Set I to be the term order_interval X x2 x1.

Apply (xm (I = Empty)) to the current goal.

Assume HIEmpty: I = Empty.

Set U0 to be the term open_ray_lower X x1.

Set V0 to be the term open_ray_upper X x2.

We use V0 to witness the existential quantifier.

We use U0 to witness the existential quantifier.

We will prove V0 ∈ order_topology X ∧ U0 ∈ order_topology X ∧ x1 ∈ V0 ∧ x2 ∈ U0 ∧ V0 ∩ U0 = Empty.

Apply andI to the current goal.

We prove the intermediate claim HVsub: V0 ∈ open_rays_subbasis X.

An exact proof term for the current goal is (open_ray_upper_in_open_rays_subbasis X x2 Hx2X).

An exact proof term for the current goal is ((open_rays_subbasis_sub_order_topology X Hso) V0 HVsub).

We prove the intermediate claim HUsub: U0 ∈ open_rays_subbasis X.

An exact proof term for the current goal is (open_ray_lower_in_open_rays_subbasis X x1 Hx1X).

An exact proof term for the current goal is ((open_rays_subbasis_sub_order_topology X Hso) U0 HUsub).

We will prove x1 ∈ V0.

An exact proof term for the current goal is (SepI X (λt : set ⇒ order_rel X x2 t) x1 Hx1X H21).

We will prove x2 ∈ U0.

An exact proof term for the current goal is (SepI X (λt : set ⇒ order_rel X t x1) x2 Hx2X H21).

We will prove V0 ∩ U0 = Empty.

Apply set_ext to the current goal.

Let y be given.

Assume Hy: y ∈ V0 ∩ U0.

We will prove y ∈ Empty.

We prove the intermediate claim HyV: y ∈ V0.

An exact proof term for the current goal is (binintersectE1 V0 U0 y Hy).

We prove the intermediate claim HyU: y ∈ U0.

An exact proof term for the current goal is (binintersectE2 V0 U0 y Hy).

We prove the intermediate claim HyX: y ∈ X.

An exact proof term for the current goal is (SepE1 X (λt : set ⇒ order_rel X t x1) y HyU).

We prove the intermediate claim Hylt1: order_rel X y x1.

An exact proof term for the current goal is (SepE2 X (λt : set ⇒ order_rel X t x1) y HyU).

We prove the intermediate claim H2lty: order_rel X x2 y.

An exact proof term for the current goal is (SepE2 X (λt : set ⇒ order_rel X x2 t) y HyV).

We prove the intermediate claim HyI: y ∈ I.

An exact proof term for the current goal is (SepI X (λt : set ⇒ order_rel X x2 t ∧ order_rel X t x1) y HyX (andI (order_rel X x2 y) (order_rel X y x1) H2lty Hylt1)).

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

An exact proof term for the current goal is HyI.

Let y be given.

Assume Hy: y ∈ Empty.

We will prove y ∈ V0 ∩ U0.

Apply FalseE to the current goal.

An exact proof term for the current goal is (EmptyE y Hy).

Assume HInon: ¬ (I = Empty).

We prove the intermediate claim HIne: I ≠ Empty.

Assume HIeq: I = Empty.

An exact proof term for the current goal is (HInon HIeq).

Apply (nonempty_has_element I HIne) to the current goal.

Let c be given.

Assume HcI: c ∈ I.

Set U0 to be the term open_ray_lower X c.

Set V0 to be the term open_ray_upper X c.

We use V0 to witness the existential quantifier.

We use U0 to witness the existential quantifier.

We will prove V0 ∈ order_topology X ∧ U0 ∈ order_topology X ∧ x1 ∈ V0 ∧ x2 ∈ U0 ∧ V0 ∩ U0 = Empty.

We prove the intermediate claim HcX: c ∈ X.

An exact proof term for the current goal is (SepE1 X (λt : set ⇒ order_rel X x2 t ∧ order_rel X t x1) c HcI).

We prove the intermediate claim HcProp: order_rel X x2 c ∧ order_rel X c x1.

An exact proof term for the current goal is (SepE2 X (λt : set ⇒ order_rel X x2 t ∧ order_rel X t x1) c HcI).

We prove the intermediate claim Hx2c: order_rel X x2 c.

An exact proof term for the current goal is (andEL (order_rel X x2 c) (order_rel X c x1) HcProp).

We prove the intermediate claim Hcx1: order_rel X c x1.

An exact proof term for the current goal is (andER (order_rel X x2 c) (order_rel X c x1) HcProp).

Apply andI to the current goal.

We prove the intermediate claim HVsub: V0 ∈ open_rays_subbasis X.

An exact proof term for the current goal is (open_ray_upper_in_open_rays_subbasis X c HcX).

An exact proof term for the current goal is ((open_rays_subbasis_sub_order_topology X Hso) V0 HVsub).

We prove the intermediate claim HUsub: U0 ∈ open_rays_subbasis X.

An exact proof term for the current goal is (open_ray_lower_in_open_rays_subbasis X c HcX).

An exact proof term for the current goal is ((open_rays_subbasis_sub_order_topology X Hso) U0 HUsub).

We will prove x1 ∈ V0.

An exact proof term for the current goal is (SepI X (λt : set ⇒ order_rel X c t) x1 Hx1X Hcx1).

We will prove x2 ∈ U0.

An exact proof term for the current goal is (SepI X (λt : set ⇒ order_rel X t c) x2 Hx2X Hx2c).

We will prove V0 ∩ U0 = Empty.

Apply set_ext to the current goal.

Let y be given.

Assume Hy: y ∈ V0 ∩ U0.

We will prove y ∈ Empty.

We prove the intermediate claim HyV: y ∈ V0.

An exact proof term for the current goal is (binintersectE1 V0 U0 y Hy).

We prove the intermediate claim HyU: y ∈ U0.

An exact proof term for the current goal is (binintersectE2 V0 U0 y Hy).

We prove the intermediate claim HyX: y ∈ X.

An exact proof term for the current goal is (SepE1 X (λt : set ⇒ order_rel X t c) y HyU).

We prove the intermediate claim Hyc: order_rel X y c.

An exact proof term for the current goal is (SepE2 X (λt : set ⇒ order_rel X t c) y HyU).

We prove the intermediate claim Hcy: order_rel X c y.

An exact proof term for the current goal is (SepE2 X (λt : set ⇒ order_rel X c t) y HyV).

We prove the intermediate claim Hyy: order_rel X y y.

An exact proof term for the current goal is (order_rel_trans X y c y Hso HyX HcX HyX Hyc Hcy).

Apply FalseE to the current goal.

An exact proof term for the current goal is (order_rel_irref X y Hyy).

Let y be given.

Assume Hy: y ∈ Empty.

We will prove y ∈ V0 ∩ U0.

Apply FalseE to the current goal.

An exact proof term for the current goal is (EmptyE y Hy).