Let p be given.

Assume HpX: p ∈ X.

We will prove p ∈ closure_of X Tx D.

We prove the intermediate claim Hcliff: p ∈ closure_of X Tx D ↔ (∀U ∈ Tx, p ∈ U → U ∩ D ≠ Empty).

An exact proof term for the current goal is (closure_characterization X Tx D p HTx HpX).

Apply (iffER (p ∈ closure_of X Tx D) (∀U ∈ Tx, p ∈ U → U ∩ D ≠ Empty) Hcliff) to the current goal.

We will prove ∀U ∈ Tx, p ∈ U → U ∩ D ≠ Empty.

Let U be given.

Assume HU: U ∈ Tx.

Assume HpU: p ∈ U.

We prove the intermediate claim Hb0: ∃b0 ∈ B, p ∈ b0 ∧ b0 ⊆ U.

We prove the intermediate claim HdefT: Tx = generated_topology X B.

Use reflexivity.

We prove the intermediate claim HUgen: U ∈ generated_topology X B.

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

An exact proof term for the current goal is HU.

An exact proof term for the current goal is (generated_topology_local_refine X B U p HUgen HpU).

Apply Hb0 to the current goal.

Let b0 be given.

Assume Hb0pair.

We prove the intermediate claim Hb0B: b0 ∈ B.

An exact proof term for the current goal is (andEL (b0 ∈ B) (p ∈ b0 ∧ b0 ⊆ U) Hb0pair).

We prove the intermediate claim Hb0prop: p ∈ b0 ∧ b0 ⊆ U.

An exact proof term for the current goal is (andER (b0 ∈ B) (p ∈ b0 ∧ b0 ⊆ U) Hb0pair).

We prove the intermediate claim Hpb0: p ∈ b0.

An exact proof term for the current goal is (andEL (p ∈ b0) (b0 ⊆ U) Hb0prop).

We prove the intermediate claim Hb0subU: b0 ⊆ U.

An exact proof term for the current goal is (andER (p ∈ b0) (b0 ⊆ U) Hb0prop).

We prove the intermediate claim HexU0: ∃U0 ∈ Sorgenfrey_topology, b0 ∈ {rectangle_set U0 V|V ∈ Sorgenfrey_topology}.

An exact proof term for the current goal is (famunionE Sorgenfrey_topology (λU0 : set ⇒ {rectangle_set U0 V|V ∈ Sorgenfrey_topology}) b0 Hb0B).

Apply HexU0 to the current goal.

Let U0 be given.

Assume HU0pair.

We prove the intermediate claim HU0open: U0 ∈ Sorgenfrey_topology.

An exact proof term for the current goal is (andEL (U0 ∈ Sorgenfrey_topology) (b0 ∈ {rectangle_set U0 V|V ∈ Sorgenfrey_topology}) HU0pair).

We prove the intermediate claim Hb0fam: b0 ∈ {rectangle_set U0 V|V ∈ Sorgenfrey_topology}.

An exact proof term for the current goal is (andER (U0 ∈ Sorgenfrey_topology) (b0 ∈ {rectangle_set U0 V|V ∈ Sorgenfrey_topology}) HU0pair).

We prove the intermediate claim HexV0: ∃V0 ∈ Sorgenfrey_topology, b0 = rectangle_set U0 V0.

An exact proof term for the current goal is (ReplE Sorgenfrey_topology (λV0 : set ⇒ rectangle_set U0 V0) b0 Hb0fam).

Apply HexV0 to the current goal.

Let V0 be given.

Assume HV0pair.

We prove the intermediate claim HV0open: V0 ∈ Sorgenfrey_topology.

An exact proof term for the current goal is (andEL (V0 ∈ Sorgenfrey_topology) (b0 = rectangle_set U0 V0) HV0pair).

We prove the intermediate claim Hb0eq: b0 = rectangle_set U0 V0.

An exact proof term for the current goal is (andER (V0 ∈ Sorgenfrey_topology) (b0 = rectangle_set U0 V0) HV0pair).

We prove the intermediate claim HpUV: p ∈ setprod U0 V0.

rewrite the current goal using (rectangle_set_def U0 V0) (from right to left).

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

An exact proof term for the current goal is Hpb0.

We prove the intermediate claim Hp0U0: proj0 p ∈ U0.

An exact proof term for the current goal is (proj0_Sigma U0 (λ_ : set ⇒ V0) p HpUV).

We prove the intermediate claim Hp1V0: proj1 p ∈ V0.

An exact proof term for the current goal is (proj1_Sigma U0 (λ_ : set ⇒ V0) p HpUV).

We prove the intermediate claim HU0ne: U0 ≠ Empty.

An exact proof term for the current goal is (elem_implies_nonempty U0 (proj0 p) Hp0U0).

We prove the intermediate claim HV0ne: V0 ≠ Empty.

An exact proof term for the current goal is (elem_implies_nonempty V0 (proj1 p) Hp1V0).

We prove the intermediate claim HQdense: closure_of Sorgenfrey_line Sorgenfrey_topology rational_numbers = Sorgenfrey_line.

An exact proof term for the current goal is Sorgenfrey_line_rationals_dense.

We prove the intermediate claim HU0meet: U0 ∩ rational_numbers ≠ Empty.

An exact proof term for the current goal is (dense_in_meets_nonempty_open rational_numbers Sorgenfrey_line Sorgenfrey_topology U0 HTline HQdense HU0open HU0ne).

We prove the intermediate claim HV0meet: V0 ∩ rational_numbers ≠ Empty.

An exact proof term for the current goal is (dense_in_meets_nonempty_open rational_numbers Sorgenfrey_line Sorgenfrey_topology V0 HTline HQdense HV0open HV0ne).

We prove the intermediate claim Hexq1: ∃q1 : set, q1 ∈ U0 ∩ rational_numbers.

An exact proof term for the current goal is (nonempty_has_element (U0 ∩ rational_numbers) HU0meet).

We prove the intermediate claim Hexq2: ∃q2 : set, q2 ∈ V0 ∩ rational_numbers.

An exact proof term for the current goal is (nonempty_has_element (V0 ∩ rational_numbers) HV0meet).

Apply Hexq1 to the current goal.

Let q1 be given.

Assume Hq1: q1 ∈ U0 ∩ rational_numbers.

Apply Hexq2 to the current goal.

Let q2 be given.

Assume Hq2: q2 ∈ V0 ∩ rational_numbers.

We prove the intermediate claim Hq1U0: q1 ∈ U0.

An exact proof term for the current goal is (binintersectE1 U0 rational_numbers q1 Hq1).

We prove the intermediate claim Hq1Q: q1 ∈ rational_numbers.

An exact proof term for the current goal is (binintersectE2 U0 rational_numbers q1 Hq1).

We prove the intermediate claim Hq2V0: q2 ∈ V0.

An exact proof term for the current goal is (binintersectE1 V0 rational_numbers q2 Hq2).

We prove the intermediate claim Hq2Q: q2 ∈ rational_numbers.

An exact proof term for the current goal is (binintersectE2 V0 rational_numbers q2 Hq2).

Set r to be the term (q1,q2).

We prove the intermediate claim HrB0: r ∈ b0.

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

An exact proof term for the current goal is (tuple_2_rectangle_set U0 V0 q1 q2 Hq1U0 Hq2V0).

We prove the intermediate claim HrU: r ∈ U.

An exact proof term for the current goal is (Hb0subU r HrB0).

We prove the intermediate claim HrD: r ∈ D.

An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma rational_numbers rational_numbers q1 q2 Hq1Q Hq2Q).

Apply (elem_implies_nonempty (U ∩ D) r) to the current goal.

An exact proof term for the current goal is (binintersectI U D r HrU HrD).