Let U be given.

Assume HU: open_cover Sorgenfrey_line Sorgenfrey_topology U.

We prove the intermediate claim HUopen: ∀u : set, u ∈ U → u ∈ Sorgenfrey_topology.

An exact proof term for the current goal is (andEL (∀u0 : set, u0 ∈ U → u0 ∈ Sorgenfrey_topology) (covers Sorgenfrey_line U) HU).

We prove the intermediate claim HUcov: covers Sorgenfrey_line U.

An exact proof term for the current goal is (andER (∀u0 : set, u0 ∈ U → u0 ∈ Sorgenfrey_topology) (covers Sorgenfrey_line U) HU).

We prove the intermediate claim Hcover_refines_basis: ∀x : set, x ∈ Sorgenfrey_line → ∃u : set, u ∈ U ∧ x ∈ u ∧ ∃b ∈ R_lower_limit_basis, x ∈ b ∧ b ⊆ u.

Let x be given.

Assume HxR: x ∈ Sorgenfrey_line.

We prove the intermediate claim Hexu: ∃u : set, u ∈ U ∧ x ∈ u.

An exact proof term for the current goal is (HUcov x HxR).

Set u0 to be the term Eps_i (λu : set ⇒ u ∈ U ∧ x ∈ u).

We prove the intermediate claim Hu0spec: u0 ∈ U ∧ x ∈ u0.

An exact proof term for the current goal is (Eps_i_ex (λu : set ⇒ u ∈ U ∧ x ∈ u) Hexu).

We prove the intermediate claim Hu0U: u0 ∈ U.

An exact proof term for the current goal is (andEL (u0 ∈ U) (x ∈ u0) Hu0spec).

We prove the intermediate claim Hxu0: x ∈ u0.

An exact proof term for the current goal is (andER (u0 ∈ U) (x ∈ u0) Hu0spec).

We prove the intermediate claim Hu0Top: u0 ∈ generated_topology R R_lower_limit_basis.

An exact proof term for the current goal is (HUopen u0 Hu0U).

We prove the intermediate claim Hu0Prop: ∀y : set, y ∈ u0 → ∃b ∈ R_lower_limit_basis, y ∈ b ∧ b ⊆ u0.

Let y be given.

Assume Hy: y ∈ u0.

An exact proof term for the current goal is (generated_topology_local_refine R R_lower_limit_basis u0 y Hu0Top Hy).

We prove the intermediate claim Hexb: ∃b ∈ R_lower_limit_basis, x ∈ b ∧ b ⊆ u0.

An exact proof term for the current goal is (Hu0Prop x Hxu0).

We use u0 to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Hu0U.

An exact proof term for the current goal is Hxu0.

An exact proof term for the current goal is Hexb.

We prove the intermediate claim Hcover_refines_halfopen_at_x: ∀x : set, x ∈ Sorgenfrey_line → ∃u : set, u ∈ U ∧ x ∈ u ∧ ∃bb ∈ R, Rlt x bb ∧ halfopen_interval_left x bb ⊆ u.

Let x be given.

Assume HxR: x ∈ Sorgenfrey_line.

We prove the intermediate claim Hexu: ∃u : set, u ∈ U ∧ x ∈ u ∧ ∃b ∈ R_lower_limit_basis, x ∈ b ∧ b ⊆ u.

An exact proof term for the current goal is (Hcover_refines_basis x HxR).

Apply Hexu to the current goal.

Let u0 be given.

Assume Hu0spec.

Apply Hu0spec to the current goal.

Assume Hu0left Hexb.

Apply Hu0left to the current goal.

Assume Hu0U Hxu0.

Apply Hexb to the current goal.

Let b0 be given.

Assume Hb0spec.

Apply Hb0spec to the current goal.

Assume Hb0B Hb0rest.

Apply Hb0rest to the current goal.

Assume Hxb0 Hb0subU0.

We prove the intermediate claim Hexa: ∃a ∈ R, b0 ∈ {halfopen_interval_left a bb|bb ∈ R}.

An exact proof term for the current goal is (famunionE R (λa0 : set ⇒ {halfopen_interval_left a0 bb|bb ∈ R}) b0 Hb0B).

Apply Hexa to the current goal.

Let a be given.

Assume Hapair.

We prove the intermediate claim HaR: a ∈ R.

An exact proof term for the current goal is (andEL (a ∈ R) (b0 ∈ {halfopen_interval_left a bb|bb ∈ R}) Hapair).

We prove the intermediate claim Hb0fam: b0 ∈ {halfopen_interval_left a bb|bb ∈ R}.

An exact proof term for the current goal is (andER (a ∈ R) (b0 ∈ {halfopen_interval_left a bb|bb ∈ R}) Hapair).

We prove the intermediate claim Hexbb: ∃bb ∈ R, b0 = halfopen_interval_left a bb.

An exact proof term for the current goal is (ReplE R (λbb0 : set ⇒ halfopen_interval_left a bb0) b0 Hb0fam).

Apply Hexbb to the current goal.

Let bb be given.

Assume Hbbpair.

We prove the intermediate claim HbbR: bb ∈ R.

An exact proof term for the current goal is (andEL (bb ∈ R) (b0 = halfopen_interval_left a bb) Hbbpair).

We prove the intermediate claim Hb0eq: b0 = halfopen_interval_left a bb.

An exact proof term for the current goal is (andER (bb ∈ R) (b0 = halfopen_interval_left a bb) Hbbpair).

We prove the intermediate claim Hxb0ab: x ∈ halfopen_interval_left a bb.

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

An exact proof term for the current goal is Hxb0.

We prove the intermediate claim Hxprop: ¬ (Rlt x a) ∧ Rlt x bb.

An exact proof term for the current goal is (SepE2 R (λt : set ⇒ ¬ (Rlt t a) ∧ Rlt t bb) x Hxb0ab).

We prove the intermediate claim Hxnltxa: ¬ (Rlt x a).

An exact proof term for the current goal is (andEL (¬ (Rlt x a)) (Rlt x bb) Hxprop).

We prove the intermediate claim Hxltbb: Rlt x bb.

An exact proof term for the current goal is (andER (¬ (Rlt x a)) (Rlt x bb) Hxprop).

We prove the intermediate claim Hax: Rle a x.

An exact proof term for the current goal is (RleI a x HaR HxR Hxnltxa).

Set b1 to be the term halfopen_interval_left x bb.

We prove the intermediate claim Hb1subb0: b1 ⊆ halfopen_interval_left a bb.

An exact proof term for the current goal is (halfopen_interval_left_leftmonotone a x bb HaR HxR HbbR Hax).

We prove the intermediate claim Hb1subU: b1 ⊆ u0.

Let y be given.

Assume Hy: y ∈ b1.

We prove the intermediate claim Hyb0: y ∈ halfopen_interval_left a bb.

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

We prove the intermediate claim Hyinb0: y ∈ b0.

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

An exact proof term for the current goal is Hyb0.

An exact proof term for the current goal is (Hb0subU0 y Hyinb0).

We use u0 to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Hu0U.

An exact proof term for the current goal is Hxu0.

We use bb to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HbbR.

Apply andI to the current goal.

An exact proof term for the current goal is Hxltbb.

An exact proof term for the current goal is Hb1subU.

Set Uof to be the term λx : set ⇒ Eps_i (λu : set ⇒ u ∈ U ∧ x ∈ u ∧ ∃b ∈ R_lower_limit_basis, x ∈ b ∧ b ⊆ u).

We prove the intermediate claim HUof_spec: ∀x : set, x ∈ Sorgenfrey_line → (Uof x ∈ U ∧ x ∈ Uof x) ∧ ∃b ∈ R_lower_limit_basis, x ∈ b ∧ b ⊆ Uof x.

Let x be given.

Assume HxR: x ∈ Sorgenfrey_line.

We prove the intermediate claim Hex: ∃u : set, u ∈ U ∧ x ∈ u ∧ ∃b ∈ R_lower_limit_basis, x ∈ b ∧ b ⊆ u.

An exact proof term for the current goal is (Hcover_refines_basis x HxR).

Apply Hex to the current goal.

Let u0 be given.

Assume Hu0spec.

We prove the intermediate claim HUsel: (Uof x ∈ U ∧ x ∈ Uof x) ∧ ∃b ∈ R_lower_limit_basis, x ∈ b ∧ b ⊆ Uof x.

An exact proof term for the current goal is (Eps_i_ax (λu : set ⇒ u ∈ U ∧ x ∈ u ∧ ∃b ∈ R_lower_limit_basis, x ∈ b ∧ b ⊆ u) u0 Hu0spec).

An exact proof term for the current goal is HUsel.

Set Bof to be the term λx : set ⇒ Eps_i (λb : set ⇒ b ∈ R_lower_limit_basis ∧ x ∈ b ∧ b ⊆ Uof x).

We prove the intermediate claim HBof_spec: ∀x : set, x ∈ Sorgenfrey_line → (Bof x ∈ R_lower_limit_basis ∧ x ∈ Bof x) ∧ Bof x ⊆ Uof x.

Let x be given.

Assume HxR: x ∈ Sorgenfrey_line.

We prove the intermediate claim HUtrip: (Uof x ∈ U ∧ x ∈ Uof x) ∧ ∃b ∈ R_lower_limit_basis, x ∈ b ∧ b ⊆ Uof x.

An exact proof term for the current goal is (HUof_spec x HxR).

We prove the intermediate claim Hexb: ∃b ∈ R_lower_limit_basis, x ∈ b ∧ b ⊆ Uof x.

An exact proof term for the current goal is (andER (Uof x ∈ U ∧ x ∈ Uof x) (∃b ∈ R_lower_limit_basis, x ∈ b ∧ b ⊆ Uof x) HUtrip).

Apply Hexb to the current goal.

Let b0 be given.

Assume Hb0pair.

We prove the intermediate claim Hb0B: b0 ∈ R_lower_limit_basis.

An exact proof term for the current goal is (andEL (b0 ∈ R_lower_limit_basis) (x ∈ b0 ∧ b0 ⊆ Uof x) Hb0pair).

We prove the intermediate claim Hb0rest: x ∈ b0 ∧ b0 ⊆ Uof x.

An exact proof term for the current goal is (andER (b0 ∈ R_lower_limit_basis) (x ∈ b0 ∧ b0 ⊆ Uof x) Hb0pair).

We prove the intermediate claim Hxb0: x ∈ b0.

An exact proof term for the current goal is (andEL (x ∈ b0) (b0 ⊆ Uof x) Hb0rest).

We prove the intermediate claim Hb0subU: b0 ⊆ Uof x.

An exact proof term for the current goal is (andER (x ∈ b0) (b0 ⊆ Uof x) Hb0rest).

An exact proof term for the current goal is (Eps_i_ax (λb : set ⇒ b ∈ R_lower_limit_basis ∧ x ∈ b ∧ b ⊆ Uof x) b0 (andI (b0 ∈ R_lower_limit_basis ∧ x ∈ b0) (b0 ⊆ Uof x) (andI (b0 ∈ R_lower_limit_basis) (x ∈ b0) Hb0B Hxb0) Hb0subU)).

Set Aof to be the term λx : set ⇒ Eps_i (λa : set ⇒ a ∈ R ∧ Bof x ∈ {halfopen_interval_left a bb|bb ∈ R}).

We prove the intermediate claim HAof_spec: ∀x : set, x ∈ Sorgenfrey_line → Aof x ∈ R ∧ Bof x ∈ {halfopen_interval_left (Aof x) bb|bb ∈ R}.

Let x be given.

Assume HxR: x ∈ Sorgenfrey_line.

We prove the intermediate claim HBleft: Bof x ∈ R_lower_limit_basis ∧ x ∈ Bof x.

An exact proof term for the current goal is (andEL (Bof x ∈ R_lower_limit_basis ∧ x ∈ Bof x) (Bof x ⊆ Uof x) (HBof_spec x HxR)).

We prove the intermediate claim HbB: Bof x ∈ R_lower_limit_basis.

An exact proof term for the current goal is (andEL (Bof x ∈ R_lower_limit_basis) (x ∈ Bof x) HBleft).

We prove the intermediate claim Hexa: ∃a ∈ R, Bof x ∈ {halfopen_interval_left a bb|bb ∈ R}.

An exact proof term for the current goal is (famunionE R (λa0 : set ⇒ {halfopen_interval_left a0 bb|bb ∈ R}) (Bof x) HbB).

Apply Hexa to the current goal.

Let a be given.

Assume Hapair.

We prove the intermediate claim HaR: a ∈ R.

An exact proof term for the current goal is (andEL (a ∈ R) (Bof x ∈ {halfopen_interval_left a bb|bb ∈ R}) Hapair).

We prove the intermediate claim HbFam: Bof x ∈ {halfopen_interval_left a bb|bb ∈ R}.

An exact proof term for the current goal is (andER (a ∈ R) (Bof x ∈ {halfopen_interval_left a bb|bb ∈ R}) Hapair).

An exact proof term for the current goal is (Eps_i_ax (λa0 : set ⇒ a0 ∈ R ∧ Bof x ∈ {halfopen_interval_left a0 bb|bb ∈ R}) a (andI (a ∈ R) (Bof x ∈ {halfopen_interval_left a bb|bb ∈ R}) HaR HbFam)).

Set BBof to be the term λx : set ⇒ Eps_i (λbb : set ⇒ bb ∈ R ∧ Bof x = halfopen_interval_left (Aof x) bb).

We prove the intermediate claim HBBof_spec: ∀x : set, x ∈ Sorgenfrey_line → BBof x ∈ R ∧ Bof x = halfopen_interval_left (Aof x) (BBof x).

Let x be given.

Assume HxR: x ∈ Sorgenfrey_line.

We prove the intermediate claim HA: Aof x ∈ R ∧ Bof x ∈ {halfopen_interval_left (Aof x) bb|bb ∈ R}.

An exact proof term for the current goal is (HAof_spec x HxR).

We prove the intermediate claim HBfam: Bof x ∈ {halfopen_interval_left (Aof x) bb|bb ∈ R}.

An exact proof term for the current goal is (andER (Aof x ∈ R) (Bof x ∈ {halfopen_interval_left (Aof x) bb|bb ∈ R}) HA).

We prove the intermediate claim Hexbb: ∃bb ∈ R, Bof x = halfopen_interval_left (Aof x) bb.

An exact proof term for the current goal is (ReplE R (λbb0 : set ⇒ halfopen_interval_left (Aof x) bb0) (Bof x) HBfam).

Apply Hexbb to the current goal.

Let bb be given.

Assume Hbbpair.

We prove the intermediate claim HbbR: bb ∈ R.

An exact proof term for the current goal is (andEL (bb ∈ R) (Bof x = halfopen_interval_left (Aof x) bb) Hbbpair).

We prove the intermediate claim HbEq: Bof x = halfopen_interval_left (Aof x) bb.

An exact proof term for the current goal is (andER (bb ∈ R) (Bof x = halfopen_interval_left (Aof x) bb) Hbbpair).

An exact proof term for the current goal is (Eps_i_ax (λbb0 : set ⇒ bb0 ∈ R ∧ Bof x = halfopen_interval_left (Aof x) bb0) bb (andI (bb ∈ R) (Bof x = halfopen_interval_left (Aof x) bb) HbbR HbEq)).

Set Iof to be the term λx : set ⇒ open_interval (Aof x) (BBof x).

Set FamI to be the term {Iof x|x ∈ Sorgenfrey_line}.

Set C to be the term ⋃ FamI.

Set D to be the term Sorgenfrey_line ∖ C.

Set q_of to be the term λx : set ⇒ Eps_i (λq : set ⇒ q ∈ rational_numbers ∧ q ∈ open_interval x (BBof x)).

We prove the intermediate claim HD_left_endpoint: ∀x : set, x ∈ D → Aof x = x.

Let x be given.

Assume HxD: x ∈ D.

We prove the intermediate claim HxR: x ∈ Sorgenfrey_line.

An exact proof term for the current goal is (setminusE1 Sorgenfrey_line C x HxD).

We prove the intermediate claim HxnotC: ¬ (x ∈ C).

An exact proof term for the current goal is (setminusE2 Sorgenfrey_line C x HxD).

We prove the intermediate claim HBspec: Bof x ∈ R_lower_limit_basis ∧ x ∈ Bof x ∧ Bof x ⊆ Uof x.

An exact proof term for the current goal is (HBof_spec x HxR).

We prove the intermediate claim HBleft0: Bof x ∈ R_lower_limit_basis ∧ x ∈ Bof x.

An exact proof term for the current goal is (andEL (Bof x ∈ R_lower_limit_basis ∧ x ∈ Bof x) (Bof x ⊆ Uof x) HBspec).

We prove the intermediate claim HxB: x ∈ Bof x.

An exact proof term for the current goal is (andER (Bof x ∈ R_lower_limit_basis) (x ∈ Bof x) HBleft0).

We prove the intermediate claim Hbbpair: BBof x ∈ R ∧ Bof x = halfopen_interval_left (Aof x) (BBof x).

An exact proof term for the current goal is (HBBof_spec x HxR).

We prove the intermediate claim HbbR: BBof x ∈ R.

An exact proof term for the current goal is (andEL (BBof x ∈ R) (Bof x = halfopen_interval_left (Aof x) (BBof x)) Hbbpair).

We prove the intermediate claim HbEq: Bof x = halfopen_interval_left (Aof x) (BBof x).

An exact proof term for the current goal is (andER (BBof x ∈ R) (Bof x = halfopen_interval_left (Aof x) (BBof x)) Hbbpair).

We prove the intermediate claim HxHalf: x ∈ halfopen_interval_left (Aof x) (BBof x).

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

An exact proof term for the current goal is HxB.

We prove the intermediate claim HxProp: ¬ (Rlt x (Aof x)) ∧ Rlt x (BBof x).

An exact proof term for the current goal is (SepE2 R (λt : set ⇒ ¬ (Rlt t (Aof x)) ∧ Rlt t (BBof x)) x HxHalf).

We prove the intermediate claim Hxnltxa: ¬ (Rlt x (Aof x)).

An exact proof term for the current goal is (andEL (¬ (Rlt x (Aof x))) (Rlt x (BBof x)) HxProp).

We prove the intermediate claim Hxltbb: Rlt x (BBof x).

An exact proof term for the current goal is (andER (¬ (Rlt x (Aof x))) (Rlt x (BBof x)) HxProp).

We prove the intermediate claim HIofsubC: Iof x ⊆ C.

Let y be given.

Assume Hy: y ∈ Iof x.

Apply (UnionI FamI y (Iof x)) to the current goal.

An exact proof term for the current goal is Hy.

An exact proof term for the current goal is (ReplI Sorgenfrey_line (λz : set ⇒ Iof z) x HxR).

We prove the intermediate claim HxnotIof: ¬ (x ∈ Iof x).

Assume HxI: x ∈ Iof x.

An exact proof term for the current goal is (HxnotC (HIofsubC x HxI)).

We prove the intermediate claim HxnotOpen: ¬ (x ∈ open_interval (Aof x) (BBof x)).

An exact proof term for the current goal is HxnotIof.

We prove the intermediate claim Hnltax: ¬ (Rlt (Aof x) x).

Assume Halt: Rlt (Aof x) x.

We prove the intermediate claim HxinOpen: x ∈ open_interval (Aof x) (BBof x).

An exact proof term for the current goal is (SepI R (λt : set ⇒ Rlt (Aof x) t ∧ Rlt t (BBof x)) x HxR (andI (Rlt (Aof x) x) (Rlt x (BBof x)) Halt Hxltbb)).

An exact proof term for the current goal is (HxnotOpen HxinOpen).

We prove the intermediate claim HaR: Aof x ∈ R.

An exact proof term for the current goal is (andEL (Aof x ∈ R) (Bof x ∈ {halfopen_interval_left (Aof x) bb|bb ∈ R}) (HAof_spec x HxR)).

An exact proof term for the current goal is (R_eq_of_not_Rlt (Aof x) x HaR HxR Hnltax Hxnltxa).

We prove the intermediate claim Hq_of_spec: ∀x : set, x ∈ D → q_of x ∈ rational_numbers ∧ q_of x ∈ open_interval x (BBof x).

Let x be given.

Assume HxD: x ∈ D.

We prove the intermediate claim HxR: x ∈ Sorgenfrey_line.

An exact proof term for the current goal is (setminusE1 Sorgenfrey_line C x HxD).

We prove the intermediate claim Hbpair: BBof x ∈ R ∧ Bof x = halfopen_interval_left (Aof x) (BBof x).

An exact proof term for the current goal is (HBBof_spec x HxR).

We prove the intermediate claim HbbR: BBof x ∈ R.

An exact proof term for the current goal is (andEL (BBof x ∈ R) (Bof x = halfopen_interval_left (Aof x) (BBof x)) Hbpair).

We prove the intermediate claim HBspec: Bof x ∈ R_lower_limit_basis ∧ x ∈ Bof x ∧ Bof x ⊆ Uof x.

An exact proof term for the current goal is (HBof_spec x HxR).

We prove the intermediate claim HBleft0: Bof x ∈ R_lower_limit_basis ∧ x ∈ Bof x.

An exact proof term for the current goal is (andEL (Bof x ∈ R_lower_limit_basis ∧ x ∈ Bof x) (Bof x ⊆ Uof x) HBspec).

We prove the intermediate claim HxB: x ∈ Bof x.

An exact proof term for the current goal is (andER (Bof x ∈ R_lower_limit_basis) (x ∈ Bof x) HBleft0).

We prove the intermediate claim HbEq: Bof x = halfopen_interval_left (Aof x) (BBof x).

An exact proof term for the current goal is (andER (BBof x ∈ R) (Bof x = halfopen_interval_left (Aof x) (BBof x)) Hbpair).

We prove the intermediate claim HxHalf: x ∈ halfopen_interval_left (Aof x) (BBof x).

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

An exact proof term for the current goal is HxB.

We prove the intermediate claim HxProp: ¬ (Rlt x (Aof x)) ∧ Rlt x (BBof x).

An exact proof term for the current goal is (SepE2 R (λt : set ⇒ ¬ (Rlt t (Aof x)) ∧ Rlt t (BBof x)) x HxHalf).

We prove the intermediate claim Hxltbb: Rlt x (BBof x).

An exact proof term for the current goal is (andER (¬ (Rlt x (Aof x))) (Rlt x (BBof x)) HxProp).

We prove the intermediate claim Hexq0: ∃q ∈ rational_numbers, Rlt x q ∧ Rlt q (BBof x).

An exact proof term for the current goal is (rational_dense_between_reals x (BBof x) HxR HbbR Hxltbb).

Apply Hexq0 to the current goal.

Let q be given.

Assume Hqpair.

We prove the intermediate claim HqQ: q ∈ rational_numbers.

An exact proof term for the current goal is (andEL (q ∈ rational_numbers) (Rlt x q ∧ Rlt q (BBof x)) Hqpair).

We prove the intermediate claim Hqprop: Rlt x q ∧ Rlt q (BBof x).

An exact proof term for the current goal is (andER (q ∈ rational_numbers) (Rlt x q ∧ Rlt q (BBof x)) Hqpair).

We prove the intermediate claim HqIn: q ∈ open_interval x (BBof x).

We prove the intermediate claim Hdef: open_interval x (BBof x) = {t ∈ R|Rlt x t ∧ Rlt t (BBof x)}.

Use reflexivity.

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

An exact proof term for the current goal is (SepI R (λt : set ⇒ Rlt x t ∧ Rlt t (BBof x)) q (rational_numbers_Subq_R q HqQ) Hqprop).

An exact proof term for the current goal is (Eps_i_ax (λq0 : set ⇒ q0 ∈ rational_numbers ∧ q0 ∈ open_interval x (BBof x)) q (andI (q ∈ rational_numbers) (q ∈ open_interval x (BBof x)) HqQ HqIn)).

We prove the intermediate claim Hq_inj: inj D rational_numbers q_of.

We will prove inj D rational_numbers q_of.

We will prove (∀x ∈ D, q_of x ∈ rational_numbers) ∧ (∀x y ∈ D, q_of x = q_of y → x = y).

Apply andI to the current goal.

Let x be given.

Assume HxD: x ∈ D.

An exact proof term for the current goal is (andEL (q_of x ∈ rational_numbers) (q_of x ∈ open_interval x (BBof x)) (Hq_of_spec x HxD)).

Let x be given.

Assume HxD: x ∈ D.

Let y be given.

Assume HyD: y ∈ D.

Assume Heq: q_of x = q_of y.

We prove the intermediate claim HxR: x ∈ R.

An exact proof term for the current goal is (setminusE1 Sorgenfrey_line C x HxD).

We prove the intermediate claim HyR: y ∈ R.

An exact proof term for the current goal is (setminusE1 Sorgenfrey_line C y HyD).

We prove the intermediate claim HxS: SNo x.

An exact proof term for the current goal is (real_SNo x HxR).

We prove the intermediate claim HyS: SNo y.

An exact proof term for the current goal is (real_SNo y HyR).

Apply (SNoLt_trichotomy_or_impred x y HxS HyS (x = y)) to the current goal.

Assume Hxy: x < y.

We prove the intermediate claim HxyR: Rlt x y.

An exact proof term for the current goal is (RltI x y HxR HyR Hxy).

We prove the intermediate claim HxA: Aof x = x.

An exact proof term for the current goal is (HD_left_endpoint x HxD).

We prove the intermediate claim HyA: Aof y = y.

An exact proof term for the current goal is (HD_left_endpoint y HyD).

We prove the intermediate claim Hqxp: q_of x ∈ open_interval x (BBof x).

An exact proof term for the current goal is (andER (q_of x ∈ rational_numbers) (q_of x ∈ open_interval x (BBof x)) (Hq_of_spec x HxD)).

We prove the intermediate claim Hqyp: q_of y ∈ open_interval y (BBof y).

An exact proof term for the current goal is (andER (q_of y ∈ rational_numbers) (q_of y ∈ open_interval y (BBof y)) (Hq_of_spec y HyD)).

We prove the intermediate claim HqInR: q_of x ∈ R.

An exact proof term for the current goal is (rational_numbers_Subq_R (q_of x) (andEL (q_of x ∈ rational_numbers) (q_of x ∈ open_interval x (BBof x)) (Hq_of_spec x HxD))).

We prove the intermediate claim Hqxb: Rlt x (q_of x) ∧ Rlt (q_of x) (BBof x).

An exact proof term for the current goal is (SepE2 R (λt : set ⇒ Rlt x t ∧ Rlt t (BBof x)) (q_of x) Hqxp).

We prove the intermediate claim Hqxlty: Rlt (q_of x) y.

We prove the intermediate claim HyNotC: ¬ (y ∈ C).

An exact proof term for the current goal is (setminusE2 Sorgenfrey_line C y HyD).

We prove the intermediate claim HIofsubC: Iof x ⊆ C.

Let t be given.

Assume Ht: t ∈ Iof x.

Apply (UnionI FamI t (Iof x)) to the current goal.

An exact proof term for the current goal is Ht.

An exact proof term for the current goal is (ReplI Sorgenfrey_line (λz : set ⇒ Iof z) x HxR).

We prove the intermediate claim HyNotIof: ¬ (y ∈ Iof x).

Assume HyI: y ∈ Iof x.

An exact proof term for the current goal is (HyNotC (HIofsubC y HyI)).

We prove the intermediate claim HyNotOpen: ¬ (y ∈ open_interval (Aof x) (BBof x)).

An exact proof term for the current goal is HyNotIof.

We prove the intermediate claim Hnlt: ¬ (Rlt y (BBof x)).

Assume Hyltbb: Rlt y (BBof x).

We prove the intermediate claim HyIn: y ∈ open_interval x (BBof x).

An exact proof term for the current goal is (SepI R (λt : set ⇒ Rlt x t ∧ Rlt t (BBof x)) y HyR (andI (Rlt x y) (Rlt y (BBof x)) HxyR Hyltbb)).

We prove the intermediate claim HyIn2: y ∈ open_interval (Aof x) (BBof x).

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

An exact proof term for the current goal is HyIn.

An exact proof term for the current goal is (HyNotOpen HyIn2).

We prove the intermediate claim HbbR: BBof x ∈ R.

An exact proof term for the current goal is (andEL (BBof x ∈ R) (Bof x = halfopen_interval_left (Aof x) (BBof x)) (HBBof_spec x HxR)).

We prove the intermediate claim HbbLe: Rle (BBof x) y.

An exact proof term for the current goal is (RleI (BBof x) y HbbR HyR Hnlt).

An exact proof term for the current goal is (Rlt_Rle_tra (q_of x) (BBof x) y (andER (Rlt x (q_of x)) (Rlt (q_of x) (BBof x)) Hqxb) HbbLe).

We prove the intermediate claim Hyltqy: Rlt y (q_of y).

An exact proof term for the current goal is (andEL (Rlt y (q_of y)) (Rlt (q_of y) (BBof y)) (SepE2 R (λt : set ⇒ Rlt y t ∧ Rlt t (BBof y)) (q_of y) Hqyp)).

We prove the intermediate claim Hqxltyq: Rlt (q_of x) (q_of y).

An exact proof term for the current goal is (Rlt_tra (q_of x) y (q_of y) Hqxlty Hyltqy).

We will prove x = y.

Apply FalseE to the current goal.

We prove the intermediate claim HqxQ: q_of x ∈ rational_numbers.

An exact proof term for the current goal is (andEL (q_of x ∈ rational_numbers) (q_of x ∈ open_interval x (BBof x)) (Hq_of_spec x HxD)).

We prove the intermediate claim HqxR0: q_of x ∈ R.

An exact proof term for the current goal is (rational_numbers_Subq_R (q_of x) HqxQ).

We prove the intermediate claim Hqxx: Rlt (q_of x) (q_of x).

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

An exact proof term for the current goal is Hqxltyq.

An exact proof term for the current goal is ((not_Rlt_refl (q_of x) HqxR0) Hqxx).

Assume HxyEq: x = y.

An exact proof term for the current goal is HxyEq.

Assume Hyx: y < x.

We prove the intermediate claim HyxR: Rlt y x.

An exact proof term for the current goal is (RltI y x HyR HxR Hyx).

We prove the intermediate claim Hqyp: q_of y ∈ open_interval y (BBof y).

An exact proof term for the current goal is (andER (q_of y ∈ rational_numbers) (q_of y ∈ open_interval y (BBof y)) (Hq_of_spec y HyD)).

We prove the intermediate claim Hqxp: q_of x ∈ open_interval x (BBof x).

An exact proof term for the current goal is (andER (q_of x ∈ rational_numbers) (q_of x ∈ open_interval x (BBof x)) (Hq_of_spec x HxD)).

We prove the intermediate claim Hqyb: Rlt y (q_of y) ∧ Rlt (q_of y) (BBof y).

An exact proof term for the current goal is (SepE2 R (λt : set ⇒ Rlt y t ∧ Rlt t (BBof y)) (q_of y) Hqyp).

We prove the intermediate claim Hqyltx: Rlt (q_of y) x.

We prove the intermediate claim HxNotC: ¬ (x ∈ C).

An exact proof term for the current goal is (setminusE2 Sorgenfrey_line C x HxD).

We prove the intermediate claim HIofsubC: Iof y ⊆ C.

Let t be given.

Assume Ht: t ∈ Iof y.

Apply (UnionI FamI t (Iof y)) to the current goal.

An exact proof term for the current goal is Ht.

An exact proof term for the current goal is (ReplI Sorgenfrey_line (λz : set ⇒ Iof z) y HyR).

We prove the intermediate claim HxNotIof: ¬ (x ∈ Iof y).

Assume HxI: x ∈ Iof y.

An exact proof term for the current goal is (HxNotC (HIofsubC x HxI)).

We prove the intermediate claim HxNotOpen: ¬ (x ∈ open_interval (Aof y) (BBof y)).

An exact proof term for the current goal is HxNotIof.

We prove the intermediate claim HyA: Aof y = y.

An exact proof term for the current goal is (HD_left_endpoint y HyD).

We prove the intermediate claim Hnlt: ¬ (Rlt x (BBof y)).

Assume Hxltbb: Rlt x (BBof y).

We prove the intermediate claim HxIn: x ∈ open_interval y (BBof y).

An exact proof term for the current goal is (SepI R (λt : set ⇒ Rlt y t ∧ Rlt t (BBof y)) x HxR (andI (Rlt y x) (Rlt x (BBof y)) HyxR Hxltbb)).

We prove the intermediate claim HxIn2: x ∈ open_interval (Aof y) (BBof y).

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

An exact proof term for the current goal is HxIn.

An exact proof term for the current goal is (HxNotOpen HxIn2).

We prove the intermediate claim HbbR: BBof y ∈ R.

An exact proof term for the current goal is (andEL (BBof y ∈ R) (Bof y = halfopen_interval_left (Aof y) (BBof y)) (HBBof_spec y HyR)).

We prove the intermediate claim HbbLe: Rle (BBof y) x.

An exact proof term for the current goal is (RleI (BBof y) x HbbR HxR Hnlt).

An exact proof term for the current goal is (Rlt_Rle_tra (q_of y) (BBof y) x (andER (Rlt y (q_of y)) (Rlt (q_of y) (BBof y)) Hqyb) HbbLe).

We prove the intermediate claim Hxltqx: Rlt x (q_of x).

An exact proof term for the current goal is (andEL (Rlt x (q_of x)) (Rlt (q_of x) (BBof x)) (SepE2 R (λt : set ⇒ Rlt x t ∧ Rlt t (BBof x)) (q_of x) Hqxp)).

We prove the intermediate claim Hqyltqx: Rlt (q_of y) (q_of x).

An exact proof term for the current goal is (Rlt_tra (q_of y) x (q_of x) Hqyltx Hxltqx).

We will prove x = y.

Apply FalseE to the current goal.

We prove the intermediate claim HqxQ: q_of x ∈ rational_numbers.

An exact proof term for the current goal is (andEL (q_of x ∈ rational_numbers) (q_of x ∈ open_interval x (BBof x)) (Hq_of_spec x HxD)).

We prove the intermediate claim HqxR0: q_of x ∈ R.

An exact proof term for the current goal is (rational_numbers_Subq_R (q_of x) HqxQ).

We prove the intermediate claim Hqxx: Rlt (q_of x) (q_of x).

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

An exact proof term for the current goal is Hqyltqx.

An exact proof term for the current goal is ((not_Rlt_refl (q_of x) HqxR0) Hqxx).

We prove the intermediate claim HDcount: countable_set D.

We prove the intermediate claim HeqImg: equip D {q_of x|x ∈ D}.

An exact proof term for the current goal is (inj_equip_image D rational_numbers q_of Hq_inj).

We prove the intermediate claim HimgSub: {q_of x|x ∈ D} ⊆ rational_numbers.

Let q be given.

Assume Hq: q ∈ {q_of x|x ∈ D}.

Apply (ReplE_impred D (λx0 : set ⇒ q_of x0) q Hq (q ∈ rational_numbers)) to the current goal.

Let x be given.

Assume HxD: x ∈ D.

Assume Heq: q = q_of x.

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

An exact proof term for the current goal is (andEL (q_of x ∈ rational_numbers) (q_of x ∈ open_interval x (BBof x)) (Hq_of_spec x HxD)).

We prove the intermediate claim HimgCount: countable_set {q_of x|x ∈ D}.

An exact proof term for the current goal is (Subq_countable {q_of x|x ∈ D} rational_numbers rational_numbers_countable HimgSub).

An exact proof term for the current goal is (equip_countable_set_right D {q_of x|x ∈ D} HeqImg HimgCount).

Set V0 to be the term {Uof x|x ∈ D}.

We prove the intermediate claim HV0subU: V0 ⊆ U.

Let v be given.

Assume Hv: v ∈ V0.

Apply (ReplE_impred D (λx0 : set ⇒ Uof x0) v Hv (v ∈ U)) to the current goal.

Let x be given.

Assume HxD: x ∈ D.

Assume HvEq: v = Uof x.

We prove the intermediate claim HxR: x ∈ Sorgenfrey_line.

An exact proof term for the current goal is (setminusE1 Sorgenfrey_line C x HxD).

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

We prove the intermediate claim HUleft: Uof x ∈ U ∧ x ∈ Uof x.

An exact proof term for the current goal is (andEL (Uof x ∈ U ∧ x ∈ Uof x) (∃b ∈ R_lower_limit_basis, x ∈ b ∧ b ⊆ Uof x) (HUof_spec x HxR)).

An exact proof term for the current goal is (andEL (Uof x ∈ U) (x ∈ Uof x) HUleft).

We prove the intermediate claim HV0count: countable_set V0.

An exact proof term for the current goal is (countable_image D HDcount (λx0 : set ⇒ Uof x0)).

We prove the intermediate claim HV0coversD: covers D V0.

Let x be given.

Assume HxD: x ∈ D.

We use (Uof x) to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is (ReplI D (λx0 : set ⇒ Uof x0) x HxD).

We prove the intermediate claim HxR: x ∈ Sorgenfrey_line.

An exact proof term for the current goal is (setminusE1 Sorgenfrey_line C x HxD).

We prove the intermediate claim HUleft: Uof x ∈ U ∧ x ∈ Uof x.

An exact proof term for the current goal is (andEL (Uof x ∈ U ∧ x ∈ Uof x) (∃b ∈ R_lower_limit_basis, x ∈ b ∧ b ⊆ Uof x) (HUof_spec x HxR)).

An exact proof term for the current goal is (andER (Uof x ∈ U) (x ∈ Uof x) HUleft).

Set FamC to be the term {Iof x ∩ C|x ∈ Sorgenfrey_line}.

We prove the intermediate claim HFamC_cover: open_cover C (subspace_topology R R_standard_topology C) FamC.

We will prove open_cover C (subspace_topology R R_standard_topology C) FamC.

We will prove (∀u : set, u ∈ FamC → u ∈ subspace_topology R R_standard_topology C) ∧ covers C FamC.

Apply andI to the current goal.

Let u be given.

Assume Hu: u ∈ FamC.

Apply (ReplE_impred Sorgenfrey_line (λx0 : set ⇒ Iof x0 ∩ C) u Hu (u ∈ subspace_topology R R_standard_topology C)) to the current goal.

Let x be given.

Assume HxR: x ∈ Sorgenfrey_line.

Assume Hueq: u = Iof x ∩ C.

We prove the intermediate claim HxR0: x ∈ Sorgenfrey_line.

An exact proof term for the current goal is HxR.

We prove the intermediate claim HbbR: BBof x ∈ R.

An exact proof term for the current goal is (andEL (BBof x ∈ R) (Bof x = halfopen_interval_left (Aof x) (BBof x)) (HBBof_spec x HxR0)).

We prove the intermediate claim HaR: Aof x ∈ R.

An exact proof term for the current goal is (andEL (Aof x ∈ R) (Bof x ∈ {halfopen_interval_left (Aof x) bb|bb ∈ R}) (HAof_spec x HxR0)).

We prove the intermediate claim HBspec: (Bof x ∈ R_lower_limit_basis ∧ x ∈ Bof x) ∧ Bof x ⊆ Uof x.

An exact proof term for the current goal is (HBof_spec x HxR0).

We prove the intermediate claim HBleft: Bof x ∈ R_lower_limit_basis ∧ x ∈ Bof x.

An exact proof term for the current goal is (andEL (Bof x ∈ R_lower_limit_basis ∧ x ∈ Bof x) (Bof x ⊆ Uof x) HBspec).

We prove the intermediate claim HxB: x ∈ Bof x.

An exact proof term for the current goal is (andER (Bof x ∈ R_lower_limit_basis) (x ∈ Bof x) HBleft).

We prove the intermediate claim HbEq: Bof x = halfopen_interval_left (Aof x) (BBof x).

An exact proof term for the current goal is (andER (BBof x ∈ R) (Bof x = halfopen_interval_left (Aof x) (BBof x)) (HBBof_spec x HxR0)).

We prove the intermediate claim HxHalf: x ∈ halfopen_interval_left (Aof x) (BBof x).

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

An exact proof term for the current goal is HxB.

We prove the intermediate claim HxProp: ¬ (Rlt x (Aof x)) ∧ Rlt x (BBof x).

An exact proof term for the current goal is (SepE2 R (λt : set ⇒ ¬ (Rlt t (Aof x)) ∧ Rlt t (BBof x)) x HxHalf).

We prove the intermediate claim Hxnlt: ¬ (Rlt x (Aof x)).

An exact proof term for the current goal is (andEL (¬ (Rlt x (Aof x))) (Rlt x (BBof x)) HxProp).

We prove the intermediate claim Hxlt: Rlt x (BBof x).

An exact proof term for the current goal is (andER (¬ (Rlt x (Aof x))) (Rlt x (BBof x)) HxProp).

We prove the intermediate claim Hax: Rle (Aof x) x.

An exact proof term for the current goal is (RleI (Aof x) x HaR HxR0 Hxnlt).

We prove the intermediate claim Hab: Rlt (Aof x) (BBof x).

An exact proof term for the current goal is (Rle_Rlt_tra (Aof x) x (BBof x) Hax Hxlt).

We prove the intermediate claim HopenI: open_interval (Aof x) (BBof x) ∈ R_standard_topology.

An exact proof term for the current goal is (open_interval_in_R_standard_topology (Aof x) (BBof x) Hab).

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

An exact proof term for the current goal is (subspace_topologyI R R_standard_topology C (Iof x) HopenI).

Let y be given.

Assume HyC: y ∈ C.

Apply (UnionE_impred FamI y HyC (∃u : set, u ∈ FamC ∧ y ∈ u)) to the current goal.

Let W be given.

Assume HyW: y ∈ W.

Assume HWFam: W ∈ FamI.

Apply (ReplE_impred Sorgenfrey_line (λx0 : set ⇒ Iof x0) W HWFam (∃u : set, u ∈ FamC ∧ y ∈ u)) to the current goal.

Let x be given.

Assume HxR: x ∈ Sorgenfrey_line.

Assume HWeq: W = Iof x.

We use (Iof x ∩ C) to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is (ReplI Sorgenfrey_line (λz : set ⇒ Iof z ∩ C) x HxR).

Apply binintersectI to the current goal.

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

An exact proof term for the current goal is HyW.

An exact proof term for the current goal is HyC.

We prove the intermediate claim HCsubR: C ⊆ R.

Let y be given.

Assume Hy: y ∈ C.

Apply (UnionE_impred FamI y Hy (y ∈ R)) to the current goal.

Let W be given.

Assume HyW: y ∈ W.

Assume HW: W ∈ FamI.

Apply (ReplE_impred Sorgenfrey_line (λx0 : set ⇒ Iof x0) W HW (y ∈ R)) to the current goal.

Let x be given.

Assume HxR: x ∈ Sorgenfrey_line.

Assume HWeq: W = Iof x.

We prove the intermediate claim HyI: y ∈ Iof x.

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

An exact proof term for the current goal is HyW.

An exact proof term for the current goal is (open_interval_Subq_R (Aof x) (BBof x) y HyI).

We prove the intermediate claim HtopCstd: topology_on C (subspace_topology R R_standard_topology C).

An exact proof term for the current goal is (subspace_topology_is_topology R R_standard_topology C R_standard_topology_is_topology HCsubR).

We prove the intermediate claim HsecCstd: second_countable_space C (subspace_topology R R_standard_topology C).

We prove the intermediate claim Hcap: (((∀A : set, A ⊆ R → first_countable_space R R_standard_topology → first_countable_space A (subspace_topology R R_standard_topology A)) ∧ (∀A : set, A ⊆ R → second_countable_space R R_standard_topology → second_countable_space A (subspace_topology R R_standard_topology A))) ∧ (∀I Xi : set, countable_index_set I → (∀i : set, i ∈ I → first_countable_space (space_family_set Xi i) (space_family_topology Xi i)) → first_countable_space (countable_product_space I Xi) (countable_product_topology_subbasis I Xi))) ∧ (∀I Xi : set, countable_index_set I → (∀i : set, i ∈ I → second_countable_space (space_family_set Xi i) (space_family_topology Xi i)) → second_countable_space (countable_product_space I Xi) (countable_product_topology_subbasis I Xi)).

An exact proof term for the current goal is (countability_axioms_subspace_product R R_standard_topology R_standard_topology_is_topology).

We prove the intermediate claim Hcc: (∀A : set, A ⊆ R → second_countable_space R R_standard_topology → second_countable_space A (subspace_topology R R_standard_topology A)).

Apply Hcap to the current goal.

Assume Hsubprod1 Hprod2.

Apply Hsubprod1 to the current goal.

Assume Hsub Hprod1.

Apply Hsub to the current goal.

Assume Hfc_sub Hsc_sub.

An exact proof term for the current goal is Hsc_sub.

An exact proof term for the current goal is (Hcc C HCsubR R_standard_topology_second_countable).

We prove the intermediate claim HexW: ∃W : set, countable_subcollection W FamC ∧ covers C W.

An exact proof term for the current goal is (countable_basis_implies_Lindelof C (subspace_topology R R_standard_topology C) HtopCstd HsecCstd FamC HFamC_cover).

Apply HexW to the current goal.

Let W be given.

Assume HWpair.

We prove the intermediate claim HWsub: countable_subcollection W FamC.

An exact proof term for the current goal is (andEL (countable_subcollection W FamC) (covers C W) HWpair).

We prove the intermediate claim HWcov: covers C W.

An exact proof term for the current goal is (andER (countable_subcollection W FamC) (covers C W) HWpair).

We prove the intermediate claim HWcount: countable_set W.

An exact proof term for the current goal is (andER (W ⊆ FamC) (countable_set W) HWsub).

Set pickx to be the term λw : set ⇒ Eps_i (λx : set ⇒ x ∈ Sorgenfrey_line ∧ w = Iof x ∩ C).

We prove the intermediate claim Hpickx_spec: ∀w : set, w ∈ W → pickx w ∈ Sorgenfrey_line ∧ w = Iof (pickx w) ∩ C.

Let w be given.

Assume HwW: w ∈ W.

We prove the intermediate claim HwFamC: w ∈ FamC.

An exact proof term for the current goal is ((andEL (W ⊆ FamC) (countable_set W) HWsub) w HwW).

We prove the intermediate claim Hexx: ∃x : set, x ∈ Sorgenfrey_line ∧ w = Iof x ∩ C.

Apply (ReplE_impred Sorgenfrey_line (λx0 : set ⇒ Iof x0 ∩ C) w HwFamC (∃x : set, x ∈ Sorgenfrey_line ∧ w = Iof x ∩ C)) to the current goal.

Let x be given.

Assume HxR: x ∈ Sorgenfrey_line.

Assume Hweq: w = Iof x ∩ C.

We use x to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HxR.

An exact proof term for the current goal is Hweq.

Apply Hexx to the current goal.

Let x be given.

Assume Hxpair.

An exact proof term for the current goal is (Eps_i_ax (λx0 : set ⇒ x0 ∈ Sorgenfrey_line ∧ w = Iof x0 ∩ C) x Hxpair).

Set V1 to be the term {Uof (pickx w)|w ∈ W}.

We prove the intermediate claim HV1subU: V1 ⊆ U.

Let v be given.

Assume Hv: v ∈ V1.

Apply (ReplE_impred W (λw0 : set ⇒ Uof (pickx w0)) v Hv (v ∈ U)) to the current goal.

Let w be given.

Assume HwW: w ∈ W.

Assume HvEq: v = Uof (pickx w).

We prove the intermediate claim HxR: pickx w ∈ Sorgenfrey_line.

An exact proof term for the current goal is (andEL (pickx w ∈ Sorgenfrey_line) (w = Iof (pickx w) ∩ C) (Hpickx_spec w HwW)).

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

We prove the intermediate claim HUleft: Uof (pickx w) ∈ U ∧ pickx w ∈ Uof (pickx w).

An exact proof term for the current goal is (andEL (Uof (pickx w) ∈ U ∧ pickx w ∈ Uof (pickx w)) (∃b ∈ R_lower_limit_basis, pickx w ∈ b ∧ b ⊆ Uof (pickx w)) (HUof_spec (pickx w) HxR)).

An exact proof term for the current goal is (andEL (Uof (pickx w) ∈ U) (pickx w ∈ Uof (pickx w)) HUleft).

We prove the intermediate claim HV1count: countable_set V1.

An exact proof term for the current goal is (countable_image W HWcount (λw0 : set ⇒ Uof (pickx w0))).

We prove the intermediate claim HV1coversC: covers C V1.

Let y be given.

Assume HyC: y ∈ C.

Apply (HWcov y HyC) to the current goal.

Let w be given.

Assume Hwpair.

We prove the intermediate claim HwW: w ∈ W.

An exact proof term for the current goal is (andEL (w ∈ W) (y ∈ w) Hwpair).

We prove the intermediate claim Hyw: y ∈ w.

An exact proof term for the current goal is (andER (w ∈ W) (y ∈ w) Hwpair).

We prove the intermediate claim Hxpair: pickx w ∈ Sorgenfrey_line ∧ w = Iof (pickx w) ∩ C.

An exact proof term for the current goal is (Hpickx_spec w HwW).

We prove the intermediate claim HxR: pickx w ∈ Sorgenfrey_line.

An exact proof term for the current goal is (andEL (pickx w ∈ Sorgenfrey_line) (w = Iof (pickx w) ∩ C) Hxpair).

We prove the intermediate claim Hweq: w = Iof (pickx w) ∩ C.

An exact proof term for the current goal is (andER (pickx w ∈ Sorgenfrey_line) (w = Iof (pickx w) ∩ C) Hxpair).

We prove the intermediate claim HyInI: y ∈ Iof (pickx w).

We prove the intermediate claim Hyw2: y ∈ Iof (pickx w) ∩ C.

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

An exact proof term for the current goal is Hyw.

An exact proof term for the current goal is (binintersectE1 (Iof (pickx w)) C y Hyw2).

We prove the intermediate claim HsubIU: Iof (pickx w) ⊆ Uof (pickx w).

Let t be given.

Assume HtI: t ∈ Iof (pickx w).

We prove the intermediate claim Hbbpair: BBof (pickx w) ∈ R ∧ Bof (pickx w) = halfopen_interval_left (Aof (pickx w)) (BBof (pickx w)).

An exact proof term for the current goal is (HBBof_spec (pickx w) HxR).

We prove the intermediate claim HbEq: Bof (pickx w) = halfopen_interval_left (Aof (pickx w)) (BBof (pickx w)).

An exact proof term for the current goal is (andER (BBof (pickx w) ∈ R) (Bof (pickx w) = halfopen_interval_left (Aof (pickx w)) (BBof (pickx w))) Hbbpair).

We prove the intermediate claim HBspec: (Bof (pickx w) ∈ R_lower_limit_basis ∧ pickx w ∈ Bof (pickx w)) ∧ Bof (pickx w) ⊆ Uof (pickx w).

An exact proof term for the current goal is (HBof_spec (pickx w) HxR).

We prove the intermediate claim HBsub: Bof (pickx w) ⊆ Uof (pickx w).

An exact proof term for the current goal is (andER (Bof (pickx w) ∈ R_lower_limit_basis ∧ pickx w ∈ Bof (pickx w)) (Bof (pickx w) ⊆ Uof (pickx w)) HBspec).

We prove the intermediate claim HopenSubHalf: open_interval (Aof (pickx w)) (BBof (pickx w)) ⊆ halfopen_interval_left (Aof (pickx w)) (BBof (pickx w)).

Let z be given.

Assume HzI: z ∈ open_interval (Aof (pickx w)) (BBof (pickx w)).

We prove the intermediate claim HzR: z ∈ R.

An exact proof term for the current goal is (SepE1 R (λt : set ⇒ Rlt (Aof (pickx w)) t ∧ Rlt t (BBof (pickx w))) z HzI).

We prove the intermediate claim Hzprop: Rlt (Aof (pickx w)) z ∧ Rlt z (BBof (pickx w)).

An exact proof term for the current goal is (SepE2 R (λt : set ⇒ Rlt (Aof (pickx w)) t ∧ Rlt t (BBof (pickx w))) z HzI).

We prove the intermediate claim Hza: Rlt (Aof (pickx w)) z.

An exact proof term for the current goal is (andEL (Rlt (Aof (pickx w)) z) (Rlt z (BBof (pickx w))) Hzprop).

We prove the intermediate claim Hzb: Rlt z (BBof (pickx w)).

An exact proof term for the current goal is (andER (Rlt (Aof (pickx w)) z) (Rlt z (BBof (pickx w))) Hzprop).

We prove the intermediate claim Hnlt: ¬ (Rlt z (Aof (pickx w))).

An exact proof term for the current goal is (not_Rlt_sym (Aof (pickx w)) z Hza).

An exact proof term for the current goal is (SepI R (λt : set ⇒ ¬ (Rlt t (Aof (pickx w))) ∧ Rlt t (BBof (pickx w))) z HzR (andI (¬ (Rlt z (Aof (pickx w)))) (Rlt z (BBof (pickx w))) Hnlt Hzb)).

We prove the intermediate claim HtHalf: t ∈ halfopen_interval_left (Aof (pickx w)) (BBof (pickx w)).

An exact proof term for the current goal is (HopenSubHalf t HtI).

We prove the intermediate claim HtB: t ∈ Bof (pickx w).

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

An exact proof term for the current goal is HtHalf.

An exact proof term for the current goal is (HBsub t HtB).

We use (Uof (pickx w)) to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is (ReplI W (λw0 : set ⇒ Uof (pickx w0)) w HwW).

An exact proof term for the current goal is (HsubIU y HyInI).

Set V to be the term V0 ∪ V1.

We use V to witness the existential quantifier.

Apply andI to the current goal.

We will prove countable_subcollection V U.

We will prove V ⊆ U ∧ countable_set V.

Apply andI to the current goal.

Let v be given.

Assume HvV: v ∈ V.

Apply (binunionE' V0 V1 v (v ∈ U)) to the current goal.

Assume Hv0: v ∈ V0.

An exact proof term for the current goal is (HV0subU v Hv0).

Assume Hv1: v ∈ V1.

An exact proof term for the current goal is (HV1subU v Hv1).

An exact proof term for the current goal is HvV.

An exact proof term for the current goal is (binunion_countable V0 V1 HV0count HV1count).

We will prove covers Sorgenfrey_line V.

Let x be given.

Assume HxR: x ∈ Sorgenfrey_line.

Apply (xm (x ∈ C)) to the current goal.

Assume HxC: x ∈ C.

Apply (HV1coversC x HxC) to the current goal.

Let u be given.

Assume Hupair.

We use u to witness the existential quantifier.

Apply andI to the current goal.

Apply binunionI2 to the current goal.

An exact proof term for the current goal is (andEL (u ∈ V1) (x ∈ u) Hupair).

An exact proof term for the current goal is (andER (u ∈ V1) (x ∈ u) Hupair).

Assume HxnotC: ¬ (x ∈ C).

We prove the intermediate claim HxD: x ∈ D.

An exact proof term for the current goal is (setminusI Sorgenfrey_line C x HxR HxnotC).

Apply (HV0coversD x HxD) to the current goal.

Let u be given.

Assume Hupair.

We use u to witness the existential quantifier.

Apply andI to the current goal.

Apply binunionI1 to the current goal.

An exact proof term for the current goal is (andEL (u ∈ V0) (x ∈ u) Hupair).

An exact proof term for the current goal is (andER (u ∈ V0) (x ∈ u) Hupair).