Apply (xm (X = R)) to the current goal.

Assume HXR: X = R.

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

We prove the intermediate claim Hcr: completely_regular_space R (metric_topology R R_bounded_metric).

An exact proof term for the current goal is (metric_spaces_completely_regular R R_bounded_metric R_bounded_metric_is_metric_on).

We prove the intermediate claim HregM: regular_space R (metric_topology R R_bounded_metric).

An exact proof term for the current goal is (completely_regular_space_implies_regular R (metric_topology R R_bounded_metric) Hcr).

We prove the intermediate claim HregStd: regular_space R R_standard_topology.

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

An exact proof term for the current goal is HregM.

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

An exact proof term for the current goal is HregStd.

Assume HneqR: ¬ (X = R).

Apply (xm (X = rational_numbers)) to the current goal.

Assume HXQ: X = rational_numbers.

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

Set Q to be the term rational_numbers.

Set Tord to be the term order_topology Q.

Set Tsub to be the term subspace_topology R R_standard_topology Q.

We prove the intermediate claim HQsubR: Q ⊆ R.

An exact proof term for the current goal is rational_numbers_Subq_R.

We prove the intermediate claim HRtop: topology_on R R_standard_topology.

An exact proof term for the current goal is R_standard_topology_is_topology.

We prove the intermediate claim HTsub: topology_on Q Tsub.

An exact proof term for the current goal is (subspace_topology_is_topology R R_standard_topology Q HRtop HQsubR).

We prove the intermediate claim HeqTop: Tord = Tsub.

Apply set_ext to the current goal.

Let U be given.

Assume HU: U ∈ Tord.

We will prove U ∈ Tsub.

We prove the intermediate claim HBsub: ∀b ∈ order_topology_basis Q, b ∈ Tsub.

Let b be given.

Assume Hb: b ∈ order_topology_basis Q.

Set A to be the term {I ∈ 𝒫 Q|∃a ∈ Q, ∃c ∈ Q, I = {x0 ∈ Q|order_rel Q a x0 ∧ order_rel Q x0 c}}.

Set B to be the term {I ∈ 𝒫 Q|∃c ∈ Q, I = {x0 ∈ Q|order_rel Q x0 c}}.

Set C to be the term {I ∈ 𝒫 Q|∃a ∈ Q, I = {x0 ∈ Q|order_rel Q a x0}}.

Set Bold to be the term (A ∪ B ∪ C).

We prove the intermediate claim HbIn: b ∈ (Bold ∪ {Q}).

We prove the intermediate claim Hdef: order_topology_basis Q = (Bold ∪ {Q}).

Use reflexivity.

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

An exact proof term for the current goal is Hb.

Apply (binunionE' Bold {Q} b (b ∈ Tsub)) to the current goal.

Assume HbBold: b ∈ Bold.

Apply (binunionE' (A ∪ B) C b (b ∈ Tsub)) to the current goal.

Assume HbAB: b ∈ (A ∪ B).

Apply (binunionE' A B b (b ∈ Tsub)) to the current goal.

Assume HbA: b ∈ A.

We prove the intermediate claim Hex: ∃a ∈ Q, ∃c ∈ Q, b = {x0 ∈ Q|order_rel Q a x0 ∧ order_rel Q x0 c}.

An exact proof term for the current goal is (SepE2 (𝒫 Q) (λI : set ⇒ ∃a ∈ Q, ∃c ∈ Q, I = {x0 ∈ Q|order_rel Q a x0 ∧ order_rel Q x0 c}) b HbA).

Apply Hex to the current goal.

Let a be given.

Assume Hapair.

Apply Hapair to the current goal.

Assume HaQ: a ∈ Q.

Assume Hexc: ∃c ∈ Q, b = {x0 ∈ Q|order_rel Q a x0 ∧ order_rel Q x0 c}.

Apply Hexc to the current goal.

Let c be given.

Assume Hcpair.

Apply Hcpair to the current goal.

Assume HcQ: c ∈ Q.

Assume Heq: b = {x0 ∈ Q|order_rel Q a x0 ∧ order_rel Q x0 c}.

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

We prove the intermediate claim HaR: a ∈ R.

An exact proof term for the current goal is (rational_numbers_in_R a HaQ).

We prove the intermediate claim HcR: c ∈ R.

An exact proof term for the current goal is (rational_numbers_in_R c HcQ).

We prove the intermediate claim Hopen: open_interval a c ∈ R_standard_topology.

An exact proof term for the current goal is (open_interval_in_R_standard_topology_endpoints a c HaR HcR).

We prove the intermediate claim Heq2: {x0 ∈ Q|order_rel Q a x0 ∧ order_rel Q x0 c} = open_interval a c ∩ Q.

Apply set_ext to the current goal.

Let x0 be given.

Assume Hx0: x0 ∈ {x1 ∈ Q|order_rel Q a x1 ∧ order_rel Q x1 c}.

We will prove x0 ∈ open_interval a c ∩ Q.

We prove the intermediate claim Hx0Q: x0 ∈ Q.

An exact proof term for the current goal is (SepE1 Q (λx1 : set ⇒ order_rel Q a x1 ∧ order_rel Q x1 c) x0 Hx0).

We prove the intermediate claim Hx0prop: order_rel Q a x0 ∧ order_rel Q x0 c.

An exact proof term for the current goal is (SepE2 Q (λx1 : set ⇒ order_rel Q a x1 ∧ order_rel Q x1 c) x0 Hx0).

We prove the intermediate claim Hax0: order_rel Q a x0.

An exact proof term for the current goal is (andEL (order_rel Q a x0) (order_rel Q x0 c) Hx0prop).

We prove the intermediate claim Hx0c: order_rel Q x0 c.

An exact proof term for the current goal is (andER (order_rel Q a x0) (order_rel Q x0 c) Hx0prop).

We prove the intermediate claim Hx0R: x0 ∈ R.

An exact proof term for the current goal is (rational_numbers_in_R x0 Hx0Q).

We prove the intermediate claim Hlt1: Rlt a x0.

An exact proof term for the current goal is (order_rel_Q_implies_Rlt a x0 Hax0).

We prove the intermediate claim Hlt2: Rlt x0 c.

An exact proof term for the current goal is (order_rel_Q_implies_Rlt x0 c Hx0c).

We prove the intermediate claim Hx0In: x0 ∈ open_interval a c.

An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt a z ∧ Rlt z c) x0 Hx0R (andI (Rlt a x0) (Rlt x0 c) Hlt1 Hlt2)).

An exact proof term for the current goal is (binintersectI (open_interval a c) Q x0 Hx0In Hx0Q).

Let x0 be given.

Assume Hx0: x0 ∈ open_interval a c ∩ Q.

We will prove x0 ∈ {x1 ∈ Q|order_rel Q a x1 ∧ order_rel Q x1 c}.

We prove the intermediate claim Hx0In: x0 ∈ open_interval a c.

An exact proof term for the current goal is (binintersectE1 (open_interval a c) Q x0 Hx0).

We prove the intermediate claim Hx0Q: x0 ∈ Q.

An exact proof term for the current goal is (binintersectE2 (open_interval a c) Q x0 Hx0).

We prove the intermediate claim Hx0prop: Rlt a x0 ∧ Rlt x0 c.

An exact proof term for the current goal is (SepE2 R (λz : set ⇒ Rlt a z ∧ Rlt z c) x0 Hx0In).

We prove the intermediate claim Hlt1: Rlt a x0.

An exact proof term for the current goal is (andEL (Rlt a x0) (Rlt x0 c) Hx0prop).

We prove the intermediate claim Hlt2: Rlt x0 c.

An exact proof term for the current goal is (andER (Rlt a x0) (Rlt x0 c) Hx0prop).

We prove the intermediate claim Hord1: order_rel Q a x0.

An exact proof term for the current goal is (Rlt_implies_order_rel_Q a x0 Hlt1).

We prove the intermediate claim Hord2: order_rel Q x0 c.

An exact proof term for the current goal is (Rlt_implies_order_rel_Q x0 c Hlt2).

An exact proof term for the current goal is (SepI Q (λx1 : set ⇒ order_rel Q a x1 ∧ order_rel Q x1 c) x0 Hx0Q (andI (order_rel Q a x0) (order_rel Q x0 c) Hord1 Hord2)).

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

An exact proof term for the current goal is (subspace_topologyI R R_standard_topology Q (open_interval a c) Hopen).

Assume HbB: b ∈ B.

We prove the intermediate claim Hex: ∃c ∈ Q, b = {x0 ∈ Q|order_rel Q x0 c}.

An exact proof term for the current goal is (SepE2 (𝒫 Q) (λI : set ⇒ ∃c ∈ Q, I = {x0 ∈ Q|order_rel Q x0 c}) b HbB).

Apply Hex to the current goal.

Let c be given.

Assume Hcpair.

Apply Hcpair to the current goal.

Assume HcQ: c ∈ Q.

Assume Heq: b = {x0 ∈ Q|order_rel Q x0 c}.

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

We prove the intermediate claim HcR: c ∈ R.

An exact proof term for the current goal is (rational_numbers_in_R c HcQ).

We prove the intermediate claim Hopen: {x0 ∈ R|Rlt x0 c} ∈ R_standard_topology.

An exact proof term for the current goal is (open_left_ray_in_R_standard_topology c HcR).

We prove the intermediate claim Heq2: {x0 ∈ Q|order_rel Q x0 c} = ({x0 ∈ R|Rlt x0 c} ∩ Q).

Apply set_ext to the current goal.

Let x0 be given.

Assume Hx0: x0 ∈ {x1 ∈ Q|order_rel Q x1 c}.

We will prove x0 ∈ {x1 ∈ R|Rlt x1 c} ∩ Q.

We prove the intermediate claim Hx0Q: x0 ∈ Q.

An exact proof term for the current goal is (SepE1 Q (λx1 : set ⇒ order_rel Q x1 c) x0 Hx0).

We prove the intermediate claim Hrel: order_rel Q x0 c.

An exact proof term for the current goal is (SepE2 Q (λx1 : set ⇒ order_rel Q x1 c) x0 Hx0).

We prove the intermediate claim Hlt: Rlt x0 c.

An exact proof term for the current goal is (order_rel_Q_implies_Rlt x0 c Hrel).

We prove the intermediate claim Hx0R: x0 ∈ R.

An exact proof term for the current goal is (rational_numbers_in_R x0 Hx0Q).

We prove the intermediate claim Hx0In: x0 ∈ {x1 ∈ R|Rlt x1 c}.

An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt z c) x0 Hx0R Hlt).

An exact proof term for the current goal is (binintersectI {x1 ∈ R|Rlt x1 c} Q x0 Hx0In Hx0Q).

Let x0 be given.

Assume Hx0: x0 ∈ ({x1 ∈ R|Rlt x1 c} ∩ Q).

We will prove x0 ∈ {x1 ∈ Q|order_rel Q x1 c}.

We prove the intermediate claim Hx0In: x0 ∈ {x1 ∈ R|Rlt x1 c}.

An exact proof term for the current goal is (binintersectE1 {x1 ∈ R|Rlt x1 c} Q x0 Hx0).

We prove the intermediate claim Hx0Q: x0 ∈ Q.

An exact proof term for the current goal is (binintersectE2 {x1 ∈ R|Rlt x1 c} Q x0 Hx0).

We prove the intermediate claim Hlt: Rlt x0 c.

An exact proof term for the current goal is (SepE2 R (λz : set ⇒ Rlt z c) x0 Hx0In).

We prove the intermediate claim Hrel: order_rel Q x0 c.

An exact proof term for the current goal is (Rlt_implies_order_rel_Q x0 c Hlt).

An exact proof term for the current goal is (SepI Q (λx1 : set ⇒ order_rel Q x1 c) x0 Hx0Q Hrel).

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

An exact proof term for the current goal is (subspace_topologyI R R_standard_topology Q ({x0 ∈ R|Rlt x0 c}) Hopen).

An exact proof term for the current goal is HbAB.

Assume HbC: b ∈ C.

We prove the intermediate claim Hex: ∃a ∈ Q, b = {x0 ∈ Q|order_rel Q a x0}.

An exact proof term for the current goal is (SepE2 (𝒫 Q) (λI : set ⇒ ∃a ∈ Q, I = {x0 ∈ Q|order_rel Q a x0}) b HbC).

Apply Hex to the current goal.

Let a be given.

Assume Hapair.

Apply Hapair to the current goal.

Assume HaQ: a ∈ Q.

Assume Heq: b = {x0 ∈ Q|order_rel Q a x0}.

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

We prove the intermediate claim HaR: a ∈ R.

An exact proof term for the current goal is (rational_numbers_in_R a HaQ).

We prove the intermediate claim Hopen: {x0 ∈ R|Rlt a x0} ∈ R_standard_topology.

An exact proof term for the current goal is (open_ray_in_R_standard_topology a HaR).

We prove the intermediate claim Heq2: {x0 ∈ Q|order_rel Q a x0} = ({x0 ∈ R|Rlt a x0} ∩ Q).

Apply set_ext to the current goal.

Let x0 be given.

Assume Hx0: x0 ∈ {x1 ∈ Q|order_rel Q a x1}.

We will prove x0 ∈ {x1 ∈ R|Rlt a x1} ∩ Q.

We prove the intermediate claim Hx0Q: x0 ∈ Q.

An exact proof term for the current goal is (SepE1 Q (λx1 : set ⇒ order_rel Q a x1) x0 Hx0).

We prove the intermediate claim Hrel: order_rel Q a x0.

An exact proof term for the current goal is (SepE2 Q (λx1 : set ⇒ order_rel Q a x1) x0 Hx0).

We prove the intermediate claim Hlt: Rlt a x0.

An exact proof term for the current goal is (order_rel_Q_implies_Rlt a x0 Hrel).

We prove the intermediate claim Hx0R: x0 ∈ R.

An exact proof term for the current goal is (rational_numbers_in_R x0 Hx0Q).

We prove the intermediate claim Hx0In: x0 ∈ {x1 ∈ R|Rlt a x1}.

An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt a z) x0 Hx0R Hlt).

An exact proof term for the current goal is (binintersectI {x1 ∈ R|Rlt a x1} Q x0 Hx0In Hx0Q).

Let x0 be given.

Assume Hx0: x0 ∈ ({x1 ∈ R|Rlt a x1} ∩ Q).

We will prove x0 ∈ {x1 ∈ Q|order_rel Q a x1}.

We prove the intermediate claim Hx0In: x0 ∈ {x1 ∈ R|Rlt a x1}.

An exact proof term for the current goal is (binintersectE1 {x1 ∈ R|Rlt a x1} Q x0 Hx0).

We prove the intermediate claim Hx0Q: x0 ∈ Q.

An exact proof term for the current goal is (binintersectE2 {x1 ∈ R|Rlt a x1} Q x0 Hx0).

We prove the intermediate claim Hlt: Rlt a x0.

An exact proof term for the current goal is (SepE2 R (λz : set ⇒ Rlt a z) x0 Hx0In).

We prove the intermediate claim Hrel: order_rel Q a x0.

An exact proof term for the current goal is (Rlt_implies_order_rel_Q a x0 Hlt).

An exact proof term for the current goal is (SepI Q (λx1 : set ⇒ order_rel Q a x1) x0 Hx0Q Hrel).

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

An exact proof term for the current goal is (subspace_topologyI R R_standard_topology Q ({x0 ∈ R|Rlt a x0}) Hopen).

An exact proof term for the current goal is HbBold.

Assume HbQ: b ∈ {Q}.

We prove the intermediate claim Heq: b = Q.

An exact proof term for the current goal is (SingE Q b HbQ).

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

An exact proof term for the current goal is (topology_has_X Q Tsub HTsub).

An exact proof term for the current goal is HbIn.

We prove the intermediate claim Hsub: Tord ⊆ Tsub.

An exact proof term for the current goal is (generated_topology_finer_weak Q (order_topology_basis Q) Tsub HTsub HBsub).

An exact proof term for the current goal is (Hsub U HU).

Let U be given.

Assume HU: U ∈ Tsub.

We will prove U ∈ Tord.

Set B to be the term order_topology_basis Q.

We prove the intermediate claim HsoQ: simply_ordered_set Q.

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

An exact proof term for the current goal is Hso.

We prove the intermediate claim HBasis: basis_on Q B.

An exact proof term for the current goal is (order_topology_basis_is_basis Q HsoQ).

We prove the intermediate claim Hdef: Tord = generated_topology Q B.

Use reflexivity.

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

rewrite the current goal using (lemma_generated_topology_characterization Q B HBasis) (from left to right).

We prove the intermediate claim HUpow: U ∈ 𝒫 Q.

An exact proof term for the current goal is (subspace_topology_in_Power R R_standard_topology Q U HU).

We prove the intermediate claim Hprop: ∀x ∈ U, ∃b ∈ B, x ∈ b ∧ b ⊆ U.

Let x be given.

Assume HxU: x ∈ U.

We prove the intermediate claim HexV: ∃V ∈ R_standard_topology, U = V ∩ Q.

An exact proof term for the current goal is (subspace_topologyE R R_standard_topology Q U HU).

Apply HexV to the current goal.

Let V be given.

Assume HVpair.

Apply HVpair to the current goal.

Assume HVopen: V ∈ R_standard_topology.

Assume HUeq: U = V ∩ Q.

We prove the intermediate claim HxVQ: x ∈ V ∩ Q.

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

An exact proof term for the current goal is HxU.

We prove the intermediate claim HxV: x ∈ V.

An exact proof term for the current goal is (binintersectE1 V Q x HxVQ).

We prove the intermediate claim HxQ: x ∈ Q.

An exact proof term for the current goal is (binintersectE2 V Q x HxVQ).

We prove the intermediate claim HxR: x ∈ R.

An exact proof term for the current goal is (rational_numbers_in_R x HxQ).

We prove the intermediate claim Hexab: ∃a b : set, a ∈ R ∧ b ∈ R ∧ x ∈ open_interval a b ∧ open_interval a b ⊆ V ∧ Rlt a x ∧ Rlt x b.

An exact proof term for the current goal is (R_standard_open_refine_interval V x HVopen HxV).

Apply Hexab to the current goal.

Let a be given.

Assume Hapak.

Apply Hapak to the current goal.

Let b be given.

Assume Habpack.

Apply Habpack to the current goal.

Assume Hab1 Hxltb.

Apply Hab1 to the current goal.

Assume Hab2 Haltx.

Apply Hab2 to the current goal.

Assume Hab3 HabsubV.

Apply Hab3 to the current goal.

Assume HabR HxInab.

Apply HabR to the current goal.

Assume HaR HbR.

We prove the intermediate claim HexRat: ∃q1 ∈ Q, ∃q2 ∈ Q, x ∈ open_interval q1 q2 ∧ open_interval q1 q2 ⊆ open_interval a b.

An exact proof term for the current goal is (rational_interval_refines_real_interval a b x HaR HbR HxR HxInab).

Apply HexRat to the current goal.

Let q1 be given.

Assume Hq1pair.

Apply Hq1pair to the current goal.

Assume Hq1Q: q1 ∈ Q.

Assume Hexq2: ∃q2 ∈ Q, x ∈ open_interval q1 q2 ∧ open_interval q1 q2 ⊆ open_interval a b.

Apply Hexq2 to the current goal.

Let q2 be given.

Assume Hq2pair.

Apply Hq2pair to the current goal.

Assume Hq2Q: q2 ∈ Q.

Assume Hqpair: x ∈ open_interval q1 q2 ∧ open_interval q1 q2 ⊆ open_interval a b.

Set Iq to be the term {y ∈ Q|order_rel Q q1 y ∧ order_rel Q y q2}.

We use Iq to witness the existential quantifier.

Apply andI to the current goal.

We prove the intermediate claim HIqPow: Iq ∈ 𝒫 Q.

Apply PowerI to the current goal.

Let y be given.

Assume Hy: y ∈ Iq.

An exact proof term for the current goal is (SepE1 Q (λy0 : set ⇒ order_rel Q q1 y0 ∧ order_rel Q y0 q2) y Hy).

We prove the intermediate claim HIqInA: Iq ∈ {I ∈ 𝒫 Q|∃a0 ∈ Q, ∃c0 ∈ Q, I = {x0 ∈ Q|order_rel Q a0 x0 ∧ order_rel Q x0 c0}}.

Apply (SepI (𝒫 Q) (λI : set ⇒ ∃a0 ∈ Q, ∃c0 ∈ Q, I = {x0 ∈ Q|order_rel Q a0 x0 ∧ order_rel Q x0 c0}) Iq HIqPow) to the current goal.

We use q1 to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Hq1Q.

We use q2 to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Hq2Q.

Use reflexivity.

We prove the intermediate claim HIqInB: Iq ∈ B.

Set B0 to be the term {I ∈ 𝒫 Q|∃b0 ∈ Q, I = {x0 ∈ Q|order_rel Q x0 b0}}.

Set C0 to be the term {I ∈ 𝒫 Q|∃a0 ∈ Q, I = {x0 ∈ Q|order_rel Q a0 x0}}.

Set Bold0 to be the term ({I ∈ 𝒫 Q|∃a0 ∈ Q, ∃c0 ∈ Q, I = {x0 ∈ Q|order_rel Q a0 x0 ∧ order_rel Q x0 c0}} ∪ B0 ∪ C0).

We prove the intermediate claim HIqInBold0: Iq ∈ Bold0.

An exact proof term for the current goal is (binunionI1 ({I ∈ 𝒫 Q|∃a0 ∈ Q, ∃c0 ∈ Q, I = {x0 ∈ Q|order_rel Q a0 x0 ∧ order_rel Q x0 c0}} ∪ B0) C0 Iq (binunionI1 {I ∈ 𝒫 Q|∃a0 ∈ Q, ∃c0 ∈ Q, I = {x0 ∈ Q|order_rel Q a0 x0 ∧ order_rel Q x0 c0}} B0 Iq HIqInA)).

We prove the intermediate claim HIqIn: Iq ∈ (Bold0 ∪ {Q}).

An exact proof term for the current goal is (binunionI1 Bold0 {Q} Iq HIqInBold0).

We prove the intermediate claim HdefB: B = (Bold0 ∪ {Q}).

Use reflexivity.

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

An exact proof term for the current goal is HIqIn.

An exact proof term for the current goal is HIqInB.

Apply andI to the current goal.

We prove the intermediate claim HxInI: x ∈ open_interval q1 q2.

An exact proof term for the current goal is (andEL (x ∈ open_interval q1 q2) (open_interval q1 q2 ⊆ open_interval a b) Hqpair).

We prove the intermediate claim HxQprop: Rlt q1 x ∧ Rlt x q2.

An exact proof term for the current goal is (SepE2 R (λz : set ⇒ Rlt q1 z ∧ Rlt z q2) x HxInI).

We prove the intermediate claim Hq1x: Rlt q1 x.

An exact proof term for the current goal is (andEL (Rlt q1 x) (Rlt x q2) HxQprop).

We prove the intermediate claim Hxq2: Rlt x q2.

An exact proof term for the current goal is (andER (Rlt q1 x) (Rlt x q2) HxQprop).

We prove the intermediate claim Hord1: order_rel Q q1 x.

An exact proof term for the current goal is (Rlt_implies_order_rel_Q q1 x Hq1x).

We prove the intermediate claim Hord2: order_rel Q x q2.

An exact proof term for the current goal is (Rlt_implies_order_rel_Q x q2 Hxq2).

An exact proof term for the current goal is (SepI Q (λy0 : set ⇒ order_rel Q q1 y0 ∧ order_rel Q y0 q2) x HxQ (andI (order_rel Q q1 x) (order_rel Q x q2) Hord1 Hord2)).

Let y be given.

Assume Hy: y ∈ Iq.

We will prove y ∈ U.

We prove the intermediate claim HyQ: y ∈ Q.

An exact proof term for the current goal is (SepE1 Q (λy0 : set ⇒ order_rel Q q1 y0 ∧ order_rel Q y0 q2) y Hy).

We prove the intermediate claim Hyprop: order_rel Q q1 y ∧ order_rel Q y q2.

An exact proof term for the current goal is (SepE2 Q (λy0 : set ⇒ order_rel Q q1 y0 ∧ order_rel Q y0 q2) y Hy).

We prove the intermediate claim Hq1y: order_rel Q q1 y.

An exact proof term for the current goal is (andEL (order_rel Q q1 y) (order_rel Q y q2) Hyprop).

We prove the intermediate claim Hyq2: order_rel Q y q2.

An exact proof term for the current goal is (andER (order_rel Q q1 y) (order_rel Q y q2) Hyprop).

We prove the intermediate claim HyR: y ∈ R.

An exact proof term for the current goal is (rational_numbers_in_R y HyQ).

We prove the intermediate claim Hlt1: Rlt q1 y.

An exact proof term for the current goal is (order_rel_Q_implies_Rlt q1 y Hq1y).

We prove the intermediate claim Hlt2: Rlt y q2.

An exact proof term for the current goal is (order_rel_Q_implies_Rlt y q2 Hyq2).

We prove the intermediate claim HyInIq: y ∈ open_interval q1 q2.

An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt q1 z ∧ Rlt z q2) y HyR (andI (Rlt q1 y) (Rlt y q2) Hlt1 Hlt2)).

We prove the intermediate claim HIqSubab: open_interval q1 q2 ⊆ open_interval a b.

An exact proof term for the current goal is (andER (x ∈ open_interval q1 q2) (open_interval q1 q2 ⊆ open_interval a b) Hqpair).

We prove the intermediate claim HyInab: y ∈ open_interval a b.

An exact proof term for the current goal is (HIqSubab y HyInIq).

We prove the intermediate claim HyV: y ∈ V.

An exact proof term for the current goal is (HabsubV y HyInab).

We prove the intermediate claim HyU: y ∈ V ∩ Q.

An exact proof term for the current goal is (binintersectI V Q y HyV HyQ).

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

An exact proof term for the current goal is HyU.

An exact proof term for the current goal is (SepI (𝒫 Q) (λU0 : set ⇒ ∀x0 ∈ U0, ∃b ∈ B, x0 ∈ b ∧ b ⊆ U0) U HUpow Hprop).

We prove the intermediate claim HregR: regular_space R R_standard_topology.

An exact proof term for the current goal is (completely_regular_space_implies_regular R R_standard_topology R_standard_topology_completely_regular).

We prove the intermediate claim Hall: (∀Y : set, Y ⊆ R → Hausdorff_space R R_standard_topology → Hausdorff_space Y (subspace_topology R R_standard_topology Y)) ∧ (∀I Xi : set, Hausdorff_spaces_family I Xi → Hausdorff_space (product_space I Xi) (product_topology_full I Xi)) ∧ (∀Y : set, Y ⊆ R → regular_space R R_standard_topology → regular_space Y (subspace_topology R R_standard_topology Y)) ∧ (∀I Xi : set, regular_spaces_family I Xi → regular_space (product_space I Xi) (product_topology_full I Xi)).

An exact proof term for the current goal is (separation_axioms_subspace_product R R_standard_topology HRtop).

We prove the intermediate claim H123: ((∀Y : set, Y ⊆ R → Hausdorff_space R R_standard_topology → Hausdorff_space Y (subspace_topology R R_standard_topology Y)) ∧ (∀I Xi : set, Hausdorff_spaces_family I Xi → Hausdorff_space (product_space I Xi) (product_topology_full I Xi))) ∧ (∀Y : set, Y ⊆ R → regular_space R R_standard_topology → regular_space Y (subspace_topology R R_standard_topology Y)).

An exact proof term for the current goal is (andEL (((∀Y : set, Y ⊆ R → Hausdorff_space R R_standard_topology → Hausdorff_space Y (subspace_topology R R_standard_topology Y)) ∧ (∀I Xi : set, Hausdorff_spaces_family I Xi → Hausdorff_space (product_space I Xi) (product_topology_full I Xi))) ∧ (∀Y : set, Y ⊆ R → regular_space R R_standard_topology → regular_space Y (subspace_topology R R_standard_topology Y))) (∀I Xi : set, regular_spaces_family I Xi → regular_space (product_space I Xi) (product_topology_full I Xi)) Hall).

We prove the intermediate claim HsubReg: ∀Y : set, Y ⊆ R → regular_space R R_standard_topology → regular_space Y (subspace_topology R R_standard_topology Y).

An exact proof term for the current goal is (andER ((∀Y : set, Y ⊆ R → Hausdorff_space R R_standard_topology → Hausdorff_space Y (subspace_topology R R_standard_topology Y)) ∧ (∀I Xi : set, Hausdorff_spaces_family I Xi → Hausdorff_space (product_space I Xi) (product_topology_full I Xi))) (∀Y : set, Y ⊆ R → regular_space R R_standard_topology → regular_space Y (subspace_topology R R_standard_topology Y)) H123).

We prove the intermediate claim HregQ: regular_space Q Tsub.

An exact proof term for the current goal is (HsubReg Q HQsubR HregR).

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

An exact proof term for the current goal is HregQ.

Assume HneqQ: ¬ (X = rational_numbers).

Apply (xm (X = ω)) to the current goal.

Assume HXo: X = ω.

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

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

An exact proof term for the current goal is (completely_regular_space_implies_regular ω (discrete_topology ω) (discrete_completely_regular_space ω)).

Assume HneqO: ¬ (X = ω).

Apply (xm (X = ω ∖ {0})) to the current goal.

Assume HXZ: X = ω ∖ {0}.

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

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

An exact proof term for the current goal is (completely_regular_space_implies_regular Zplus (discrete_topology Zplus) (discrete_completely_regular_space Zplus)).

Assume HneqZ: ¬ (X = ω ∖ {0}).

Apply (xm (X = setprod 2 ω)) to the current goal.

Assume HX2: X = setprod 2 ω.

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

An exact proof term for the current goal is regular_space_order_topology_setprod_2_omega.

Assume Hneq2: ¬ (X = setprod 2 ω).

Apply (xm (X = setprod R R)) to the current goal.

Assume HXRR: X = setprod R R.

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

We prove the intermediate claim HregDisc: regular_space R (discrete_topology R).

An exact proof term for the current goal is (completely_regular_space_implies_regular R (discrete_topology R) (discrete_completely_regular_space R)).

We prove the intermediate claim Hcr: completely_regular_space R (metric_topology R R_bounded_metric).

An exact proof term for the current goal is (metric_spaces_completely_regular R R_bounded_metric R_bounded_metric_is_metric_on).

We prove the intermediate claim HregM: regular_space R (metric_topology R R_bounded_metric).

An exact proof term for the current goal is (completely_regular_space_implies_regular R (metric_topology R R_bounded_metric) Hcr).

We prove the intermediate claim HregStd: regular_space R R_standard_topology.

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

An exact proof term for the current goal is HregM.

We prove the intermediate claim HregProd: regular_space (setprod R R) (product_topology R (discrete_topology R) R R_standard_topology).

An exact proof term for the current goal is (product_topology_regular R (discrete_topology R) R R_standard_topology HregDisc HregStd).

We prove the intermediate claim HeqDictProd: R2_dictionary_order_topology = product_topology R (discrete_topology R) R R_standard_topology.

An exact proof term for the current goal is (andEL (R2_dictionary_order_topology = product_topology R (discrete_topology R) R R_standard_topology) (R2_dictionary_order_topology ≠ R2_standard_topology) ex16_9_dictionary_equals_product).

We prove the intermediate claim HsoRR: simply_ordered_set (setprod R R).

An exact proof term for the current goal is simply_ordered_set_setprod_R_R.

We prove the intermediate claim HeqOrdDict: order_topology (setprod R R) = R2_dictionary_order_topology.

rewrite the current goal using (open_rays_subbasis_for_order_topology (setprod R R) HsoRR) (from right to left).

Use reflexivity.

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

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

An exact proof term for the current goal is HregProd.

Assume HneqRR: ¬ (X = setprod R R).

We prove the intermediate claim HordX: ordinal X.

Apply (Hso (ordinal X)) to the current goal.

Assume Hleft6.

Apply (Hleft6 (ordinal X)) to the current goal.

Assume Hleft5.

Apply (Hleft5 (ordinal X)) to the current goal.

Assume Hleft4.

Apply (Hleft4 (ordinal X)) to the current goal.

Assume Hleft3.

Apply (Hleft3 (ordinal X)) to the current goal.

Assume Hleft2.

Apply (Hleft2 (ordinal X)) to the current goal.

Assume HXR: X = R.