Set Tdic to be the term subspace_topology (setprod R R) R2_dictionary_order_topology ordered_square.

Set Tprod to be the term product_topology unit_interval unit_interval_topology unit_interval unit_interval_topology.

We will prove Tdic ≠ Tprod.

Assume Heq: Tdic = Tprod.

Set U to be the term ordered_square_open_strip.

We prove the intermediate claim HUdic: U ∈ Tdic.

We will prove U ∈ Tdic.

We prove the intermediate claim HUsub: U ⊆ ordered_square.

Let p be given.

Assume Hp: p ∈ U.

An exact proof term for the current goal is (SepE1 ordered_square (λp0 : set ⇒ ∃y : set, p0 = (eps_ 1,y) ∧ Rlt (eps_ 1) y ∧ ¬ (Rlt 1 y)) p Hp).

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

An exact proof term for the current goal is (PowerI ordered_square U HUsub).

Set a to be the term (eps_ 1,eps_ 1).

Set b to be the term (eps_ 1,2).

Set V to be the term {p ∈ setprod R R|order_rel (setprod R R) a p ∧ order_rel (setprod R R) p b}.

We prove the intermediate claim HVTx: V ∈ R2_dictionary_order_topology.

Set X to be the term setprod R R.

We prove the intermediate claim HS: subbasis_on X (open_rays_subbasis X).

An exact proof term for the current goal is (open_rays_subbasis_is_subbasis X).

We prove the intermediate claim HT: topology_on X R2_dictionary_order_topology.

An exact proof term for the current goal is dictionary_order_topology_is_topology.

We prove the intermediate claim HaX: a ∈ X.

An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma R R (eps_ 1) (eps_ 1) eps_1_in_R eps_1_in_R).

We prove the intermediate claim HbX: b ∈ X.

An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma R R (eps_ 1) 2 eps_1_in_R two_in_R).

Set U1 to be the term open_ray_upper X a.

Set U2 to be the term open_ray_lower X b.

We prove the intermediate claim HU1S: U1 ∈ open_rays_subbasis X.

An exact proof term for the current goal is (open_ray_upper_in_open_rays_subbasis X a HaX).

We prove the intermediate claim HU2S: U2 ∈ open_rays_subbasis X.

An exact proof term for the current goal is (open_ray_lower_in_open_rays_subbasis X b HbX).

We prove the intermediate claim HU1open: U1 ∈ R2_dictionary_order_topology.

An exact proof term for the current goal is (subbasis_elem_open_in_generated_from_subbasis X (open_rays_subbasis X) U1 HS HU1S).

We prove the intermediate claim HU2open: U2 ∈ R2_dictionary_order_topology.

An exact proof term for the current goal is (subbasis_elem_open_in_generated_from_subbasis X (open_rays_subbasis X) U2 HS HU2S).

We prove the intermediate claim HVeq: V = U1 ∩ U2.

We prove the intermediate claim HdefV: V = {p ∈ X|order_rel X a p ∧ order_rel X p b}.

Use reflexivity.

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

An exact proof term for the current goal is (open_interval_eq_rays_intersection X a b).

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

An exact proof term for the current goal is (topology_binintersect_closed X R2_dictionary_order_topology U1 U2 HT HU1open HU2open).

We prove the intermediate claim HeqU: U = V ∩ ordered_square.

Apply set_ext to the current goal.

Let p be given.

Assume HpU: p ∈ U.

We will prove p ∈ V ∩ ordered_square.

We prove the intermediate claim HpSq: p ∈ ordered_square.

An exact proof term for the current goal is (SepE1 ordered_square (λp0 : set ⇒ ∃y : set, p0 = (eps_ 1,y) ∧ Rlt (eps_ 1) y ∧ ¬ (Rlt 1 y)) p HpU).

We prove the intermediate claim Hexy: ∃y : set, p = (eps_ 1,y) ∧ Rlt (eps_ 1) y ∧ ¬ (Rlt 1 y).

An exact proof term for the current goal is (SepE2 ordered_square (λp0 : set ⇒ ∃y : set, p0 = (eps_ 1,y) ∧ Rlt (eps_ 1) y ∧ ¬ (Rlt 1 y)) p HpU).

Apply Hexy to the current goal.

Let y be given.

Assume Hyprop.

We prove the intermediate claim Hpair: (p = (eps_ 1,y) ∧ Rlt (eps_ 1) y).

An exact proof term for the current goal is (andEL (p = (eps_ 1,y) ∧ Rlt (eps_ 1) y) (¬ (Rlt 1 y)) Hyprop).

We prove the intermediate claim Hyle1: ¬ (Rlt 1 y).

An exact proof term for the current goal is (andER (p = (eps_ 1,y) ∧ Rlt (eps_ 1) y) (¬ (Rlt 1 y)) Hyprop).

We prove the intermediate claim Hpy: p = (eps_ 1,y).

An exact proof term for the current goal is (andEL (p = (eps_ 1,y)) (Rlt (eps_ 1) y) Hpair).

We prove the intermediate claim Hey: Rlt (eps_ 1) y.

An exact proof term for the current goal is (andER (p = (eps_ 1,y)) (Rlt (eps_ 1) y) Hpair).

We prove the intermediate claim Heps1R: eps_ 1 ∈ R.

An exact proof term for the current goal is (RltE_left (eps_ 1) y Hey).

We prove the intermediate claim HyR: y ∈ R.

An exact proof term for the current goal is (RltE_right (eps_ 1) y Hey).

We prove the intermediate claim HpV: p ∈ V.

We will prove p ∈ V.

We prove the intermediate claim HpRR: p ∈ setprod R R.

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

An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma R R (eps_ 1) y Heps1R HyR).

We prove the intermediate claim Hord1: order_rel (setprod R R) a p.

We will prove (setprod R R = R ∧ Rlt a p) ∨ (setprod R R = rational_numbers ∧ Rlt a p) ∨ (setprod R R = ω ∧ a ∈ p) ∨ (setprod R R = ω ∖ {0} ∧ a ∈ p) ∨ (setprod R R = setprod 2 ω ∧ ∃i m j n : set, i ∈ 2 ∧ m ∈ ω ∧ j ∈ 2 ∧ n ∈ ω ∧ a = (i,m) ∧ p = (j,n) ∧ (i ∈ j ∨ (i = j ∧ m ∈ n))) ∨ (setprod R R = setprod R R ∧ ∃a1 a2 b1 b2 : set, a = (a1,a2) ∧ p = (b1,b2) ∧ (Rlt a1 b1 ∨ (a1 = b1 ∧ Rlt a2 b2))) ∨ (ordinal (setprod R R) ∧ setprod R R ≠ R ∧ setprod R R ≠ rational_numbers ∧ setprod R R ≠ setprod 2 ω ∧ setprod R R ≠ setprod R R ∧ a ∈ p).

Apply orIL to the current goal.

Apply orIR to the current goal.

We will prove (setprod R R = setprod R R ∧ ∃a1 a2 b1 b2 : set, a = (a1,a2) ∧ p = (b1,b2) ∧ (Rlt a1 b1 ∨ (a1 = b1 ∧ Rlt a2 b2))).

Apply andI to the current goal.

Use reflexivity.

We use (eps_ 1) to witness the existential quantifier.

We use y to witness the existential quantifier.

We will prove a = (eps_ 1,eps_ 1) ∧ p = (eps_ 1,y) ∧ (Rlt (eps_ 1) (eps_ 1) ∨ ((eps_ 1) = (eps_ 1) ∧ Rlt (eps_ 1) y)).

Apply andI to the current goal.

Use reflexivity.

An exact proof term for the current goal is Hpy.

Apply orIR to the current goal.

Apply andI to the current goal.

Use reflexivity.

An exact proof term for the current goal is Hey.

We prove the intermediate claim Hord2: order_rel (setprod R R) p b.

We will prove (setprod R R = R ∧ Rlt p b) ∨ (setprod R R = rational_numbers ∧ Rlt p b) ∨ (setprod R R = ω ∧ p ∈ b) ∨ (setprod R R = ω ∖ {0} ∧ p ∈ b) ∨ (setprod R R = setprod 2 ω ∧ ∃i m j n : set, i ∈ 2 ∧ m ∈ ω ∧ j ∈ 2 ∧ n ∈ ω ∧ p = (i,m) ∧ b = (j,n) ∧ (i ∈ j ∨ (i = j ∧ m ∈ n))) ∨ (setprod R R = setprod R R ∧ ∃a1 a2 b1 b2 : set, p = (a1,a2) ∧ b = (b1,b2) ∧ (Rlt a1 b1 ∨ (a1 = b1 ∧ Rlt a2 b2))) ∨ (ordinal (setprod R R) ∧ setprod R R ≠ R ∧ setprod R R ≠ rational_numbers ∧ setprod R R ≠ setprod 2 ω ∧ setprod R R ≠ setprod R R ∧ p ∈ b).

Apply orIL to the current goal.

Apply orIR to the current goal.

We will prove (setprod R R = setprod R R ∧ ∃a1 a2 b1 b2 : set, p = (a1,a2) ∧ b = (b1,b2) ∧ (Rlt a1 b1 ∨ (a1 = b1 ∧ Rlt a2 b2))).

Apply andI to the current goal.

Use reflexivity.

We prove the intermediate claim HdefR: R = real.

Use reflexivity.

We prove the intermediate claim H1R: 1 ∈ R.

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

An exact proof term for the current goal is real_1.

We prove the intermediate claim H2R: 2 ∈ R.

We prove the intermediate claim H2real: 2 ∈ real.

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

An exact proof term for the current goal is (real_add_SNo 1 real_1 1 real_1).

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

An exact proof term for the current goal is H2real.

We prove the intermediate claim H12: Rlt 1 2.

An exact proof term for the current goal is (RltI 1 2 H1R H2R SNoLt_1_2).

We prove the intermediate claim Hy2: Rlt y 2.

We prove the intermediate claim Hyreal: y ∈ real.

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

An exact proof term for the current goal is HyR.

We prove the intermediate claim H2real: 2 ∈ real.

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

An exact proof term for the current goal is H2R.

We prove the intermediate claim HyS: SNo y.

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

We prove the intermediate claim H2S: SNo 2.

An exact proof term for the current goal is (real_SNo 2 H2real).

Apply (SNoLt_trichotomy_or_impred y 2 HyS H2S (Rlt y 2)) to the current goal.

Assume Hylt: y < 2.

An exact proof term for the current goal is (RltI y 2 HyR H2R Hylt).

Assume Hyeq: y = 2.

Apply FalseE to the current goal.

We prove the intermediate claim H1y: Rlt 1 y.

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

An exact proof term for the current goal is H12.

An exact proof term for the current goal is (Hyle1 H1y).

Assume H2lty: 2 < y.

Apply FalseE to the current goal.

We prove the intermediate claim H2y: Rlt 2 y.

An exact proof term for the current goal is (RltI 2 y H2R HyR H2lty).

We prove the intermediate claim H1y: Rlt 1 y.

An exact proof term for the current goal is (Rlt_tra 1 2 y H12 H2y).

An exact proof term for the current goal is (Hyle1 H1y).

We use (eps_ 1) to witness the existential quantifier.

We use y to witness the existential quantifier.

We use (eps_ 1) to witness the existential quantifier.

We use 2 to witness the existential quantifier.

We will prove p = (eps_ 1,y) ∧ b = (eps_ 1,2) ∧ (Rlt (eps_ 1) (eps_ 1) ∨ ((eps_ 1) = (eps_ 1) ∧ Rlt y 2)).

Apply andI to the current goal.

An exact proof term for the current goal is Hpy.

Use reflexivity.

Apply orIR to the current goal.

Apply andI to the current goal.

Use reflexivity.

An exact proof term for the current goal is Hy2.

An exact proof term for the current goal is (SepI (setprod R R) (λp0 : set ⇒ order_rel (setprod R R) a p0 ∧ order_rel (setprod R R) p0 b) p HpRR (andI (order_rel (setprod R R) a p) (order_rel (setprod R R) p b) Hord1 Hord2)).

An exact proof term for the current goal is (binintersectI V ordered_square p HpV HpSq).

Let p be given.

Assume Hp: p ∈ V ∩ ordered_square.

We will prove p ∈ U.

We prove the intermediate claim HpPair: p ∈ V ∧ p ∈ ordered_square.

An exact proof term for the current goal is (binintersectE V ordered_square p Hp).

We prove the intermediate claim HpSq: p ∈ ordered_square.

An exact proof term for the current goal is (andER (p ∈ V) (p ∈ ordered_square) HpPair).

We prove the intermediate claim Hexists: ∃y : set, p = (eps_ 1,y) ∧ Rlt (eps_ 1) y ∧ ¬ (Rlt 1 y).

We prove the intermediate claim HsqDef: ordered_square = setprod unit_interval unit_interval.

Use reflexivity.

We prove the intermediate claim HpProd: p ∈ setprod unit_interval unit_interval.

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

An exact proof term for the current goal is HpSq.

We prove the intermediate claim HpV: p ∈ V.

An exact proof term for the current goal is (andEL (p ∈ V) (p ∈ ordered_square) HpPair).

We prove the intermediate claim Hpord: order_rel (setprod R R) a p ∧ order_rel (setprod R R) p b.

An exact proof term for the current goal is (SepE2 (setprod R R) (λp0 : set ⇒ order_rel (setprod R R) a p0 ∧ order_rel (setprod R R) p0 b) p HpV).

We prove the intermediate claim Hord1: order_rel (setprod R R) a p.

An exact proof term for the current goal is (andEL (order_rel (setprod R R) a p) (order_rel (setprod R R) p b) Hpord).

We prove the intermediate claim Hord2: order_rel (setprod R R) p b.

An exact proof term for the current goal is (andER (order_rel (setprod R R) a p) (order_rel (setprod R R) p b) Hpord).

We prove the intermediate claim Hex_ap: ∃a1 a2 b1 b2 : set, a = (a1,a2) ∧ p = (b1,b2) ∧ (Rlt a1 b1 ∨ (a1 = b1 ∧ Rlt a2 b2)).

An exact proof term for the current goal is (order_rel_setprod_R_R_unfold a p Hord1).

We prove the intermediate claim Hex_pb: ∃a1 a2 b1 b2 : set, p = (a1,a2) ∧ b = (b1,b2) ∧ (Rlt a1 b1 ∨ (a1 = b1 ∧ Rlt a2 b2)).

An exact proof term for the current goal is (order_rel_setprod_R_R_unfold p b Hord2).

Set y to be the term proj1 p.

We prove the intermediate claim HyU: y ∈ unit_interval.

An exact proof term for the current goal is (proj1_Sigma unit_interval (λ_ : set ⇒ unit_interval) p HpProd).

We prove the intermediate claim Hyprop: ¬ (Rlt 1 y).

An exact proof term for the current goal is (andER (¬ (Rlt y 0)) (¬ (Rlt 1 y)) (SepE2 R (λt : set ⇒ ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t)) y HyU)).

We use y to witness the existential quantifier.

We will prove p = (eps_ 1,y) ∧ Rlt (eps_ 1) y ∧ ¬ (Rlt 1 y).

We prove the intermediate claim Heps1R: (eps_ 1) ∈ R.

We prove the intermediate claim H1omega: 1 ∈ ω.

An exact proof term for the current goal is (nat_p_omega 1 nat_1).

We prove the intermediate claim Heps1SNoS: eps_ 1 ∈ SNoS_ ω.

An exact proof term for the current goal is (SNo_eps_SNoS_omega 1 H1omega).

An exact proof term for the current goal is (SNoS_omega_real (eps_ 1) Heps1SNoS).

We prove the intermediate claim HpFirst: p = (eps_ 1,y) ∧ Rlt (eps_ 1) y.

Apply Hex_ap to the current goal.

Let a1 be given.

Assume Hex_a2.

Apply Hex_a2 to the current goal.

Let a2 be given.

Assume Hex_b1.

Apply Hex_b1 to the current goal.

Let b1 be given.

Assume Hex_b2.

Apply Hex_b2 to the current goal.

Let b2 be given.

Assume Hap.

We prove the intermediate claim Hcore1: a = (a1,a2) ∧ p = (b1,b2).

An exact proof term for the current goal is (andEL (a = (a1,a2) ∧ p = (b1,b2)) (Rlt a1 b1 ∨ (a1 = b1 ∧ Rlt a2 b2)) Hap).

We prove the intermediate claim HaEq: a = (a1,a2).

An exact proof term for the current goal is (andEL (a = (a1,a2)) (p = (b1,b2)) Hcore1).

We prove the intermediate claim HpEq: p = (b1,b2).

An exact proof term for the current goal is (andER (a = (a1,a2)) (p = (b1,b2)) Hcore1).

We prove the intermediate claim Hdisj1: Rlt a1 b1 ∨ (a1 = b1 ∧ Rlt a2 b2).

An exact proof term for the current goal is (andER (a = (a1,a2) ∧ p = (b1,b2)) (Rlt a1 b1 ∨ (a1 = b1 ∧ Rlt a2 b2)) Hap).

We prove the intermediate claim HaDef: a = (eps_ 1,eps_ 1).

Use reflexivity.

We prove the intermediate claim Ha0: a 0 = eps_ 1.

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

An exact proof term for the current goal is (tuple_2_0_eq (eps_ 1) (eps_ 1)).

We prove the intermediate claim Ha1: a 1 = eps_ 1.

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

An exact proof term for the current goal is (tuple_2_1_eq (eps_ 1) (eps_ 1)).

We prove the intermediate claim Ha0': a 0 = a1.

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

An exact proof term for the current goal is (tuple_2_0_eq a1 a2).

We prove the intermediate claim Ha1': a 1 = a2.

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

An exact proof term for the current goal is (tuple_2_1_eq a1 a2).

We prove the intermediate claim Ha1eq: a1 = eps_ 1.

We will prove a1 = eps_ 1.

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

An exact proof term for the current goal is Ha0.

We prove the intermediate claim Ha2eq: a2 = eps_ 1.

We will prove a2 = eps_ 1.

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

An exact proof term for the current goal is Ha1.

We prove the intermediate claim Hdisj1': Rlt (eps_ 1) b1 ∨ ((eps_ 1) = b1 ∧ Rlt (eps_ 1) b2).

Apply (Hdisj1 (Rlt (eps_ 1) b1 ∨ ((eps_ 1) = b1 ∧ Rlt (eps_ 1) b2))) to the current goal.

Assume Hlt: Rlt a1 b1.

Apply orIL to the current goal.

We will prove Rlt (eps_ 1) b1.

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

An exact proof term for the current goal is Hlt.

Assume Hc: a1 = b1 ∧ Rlt a2 b2.

We prove the intermediate claim Ha1b1: a1 = b1.

An exact proof term for the current goal is (andEL (a1 = b1) (Rlt a2 b2) Hc).

We prove the intermediate claim Ha2b2: Rlt a2 b2.

An exact proof term for the current goal is (andER (a1 = b1) (Rlt a2 b2) Hc).

We prove the intermediate claim Heq: (eps_ 1) = b1.

We will prove (eps_ 1) = b1.

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

An exact proof term for the current goal is Ha1b1.

We prove the intermediate claim Hltb2: Rlt (eps_ 1) b2.

We will prove Rlt (eps_ 1) b2.

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

An exact proof term for the current goal is Ha2b2.

Apply orIR to the current goal.

An exact proof term for the current goal is (andI ((eps_ 1) = b1) (Rlt (eps_ 1) b2) Heq Hltb2).

Apply Hex_pb to the current goal.

Let c1 be given.

Assume Hex_c2.

Apply Hex_c2 to the current goal.

Let c2 be given.

Assume Hex_d1.

Apply Hex_d1 to the current goal.

Let d1 be given.

Assume Hex_d2.

Apply Hex_d2 to the current goal.

Let d2 be given.

Assume Hpb.

We prove the intermediate claim Hcore2: p = (c1,c2) ∧ b = (d1,d2).

An exact proof term for the current goal is (andEL (p = (c1,c2) ∧ b = (d1,d2)) (Rlt c1 d1 ∨ (c1 = d1 ∧ Rlt c2 d2)) Hpb).

We prove the intermediate claim HpEq2: p = (c1,c2).

An exact proof term for the current goal is (andEL (p = (c1,c2)) (b = (d1,d2)) Hcore2).

We prove the intermediate claim HbEq: b = (d1,d2).

An exact proof term for the current goal is (andER (p = (c1,c2)) (b = (d1,d2)) Hcore2).

We prove the intermediate claim Hdisj2: Rlt c1 d1 ∨ (c1 = d1 ∧ Rlt c2 d2).

An exact proof term for the current goal is (andER (p = (c1,c2) ∧ b = (d1,d2)) (Rlt c1 d1 ∨ (c1 = d1 ∧ Rlt c2 d2)) Hpb).

We prove the intermediate claim Hp0b1: p 0 = b1.

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

An exact proof term for the current goal is (tuple_2_0_eq b1 b2).

We prove the intermediate claim Hp0c1: p 0 = c1.

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

An exact proof term for the current goal is (tuple_2_0_eq c1 c2).

We prove the intermediate claim Hc1eq: c1 = b1.

We will prove c1 = b1.

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

An exact proof term for the current goal is Hp0b1.

We prove the intermediate claim Hp1b2: p 1 = b2.

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

An exact proof term for the current goal is (tuple_2_1_eq b1 b2).

We prove the intermediate claim Hp1c2: p 1 = c2.

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

An exact proof term for the current goal is (tuple_2_1_eq c1 c2).

We prove the intermediate claim Hc2eq: c2 = b2.

We will prove c2 = b2.

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

An exact proof term for the current goal is Hp1b2.

We prove the intermediate claim HbDef: b = (eps_ 1,2).

Use reflexivity.

We prove the intermediate claim Hb0: b 0 = eps_ 1.

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

An exact proof term for the current goal is (tuple_2_0_eq (eps_ 1) 2).

We prove the intermediate claim Hb1: b 1 = 2.

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

An exact proof term for the current goal is (tuple_2_1_eq (eps_ 1) 2).

We prove the intermediate claim Hb0': b 0 = d1.

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

An exact proof term for the current goal is (tuple_2_0_eq d1 d2).

We prove the intermediate claim Hb1': b 1 = d2.

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

An exact proof term for the current goal is (tuple_2_1_eq d1 d2).

We prove the intermediate claim Hd1eq: d1 = eps_ 1.

We will prove d1 = eps_ 1.

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

An exact proof term for the current goal is Hb0.

We prove the intermediate claim Hd2eq: d2 = 2.

We will prove d2 = 2.

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

An exact proof term for the current goal is Hb1.

We prove the intermediate claim Hdisj2': Rlt b1 (eps_ 1) ∨ (b1 = eps_ 1 ∧ Rlt b2 2).

Apply (Hdisj2 (Rlt b1 (eps_ 1) ∨ (b1 = eps_ 1 ∧ Rlt b2 2))) to the current goal.

Assume Hlt: Rlt c1 d1.

Apply orIL to the current goal.

We will prove Rlt b1 (eps_ 1).

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

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

An exact proof term for the current goal is Hlt.

Assume Hc: c1 = d1 ∧ Rlt c2 d2.

We prove the intermediate claim Hc1d1: c1 = d1.

An exact proof term for the current goal is (andEL (c1 = d1) (Rlt c2 d2) Hc).

We prove the intermediate claim Hc2d2: Rlt c2 d2.

An exact proof term for the current goal is (andER (c1 = d1) (Rlt c2 d2) Hc).

We prove the intermediate claim Hb1eq: b1 = eps_ 1.

We will prove b1 = eps_ 1.

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

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

An exact proof term for the current goal is Hc1d1.

We prove the intermediate claim Hb2lt: Rlt b2 2.

We will prove Rlt b2 2.

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

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

An exact proof term for the current goal is Hc2d2.

Apply orIR to the current goal.

An exact proof term for the current goal is (andI (b1 = eps_ 1) (Rlt b2 2) Hb1eq Hb2lt).

We prove the intermediate claim HyP1: y = p 1.

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

Use reflexivity.

We prove the intermediate claim HyEq: y = b2.

We will prove y = b2.

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

An exact proof term for the current goal is Hp1b2.

Apply (Hdisj1' (p = (eps_ 1,y) ∧ Rlt (eps_ 1) y)) to the current goal.

Assume Hlt: Rlt (eps_ 1) b1.

Apply FalseE to the current goal.

Apply (Hdisj2' False) to the current goal.

Assume Hlt2: Rlt b1 (eps_ 1).

An exact proof term for the current goal is ((not_Rlt_sym (eps_ 1) b1 Hlt) Hlt2).

Assume Hc: b1 = eps_ 1 ∧ Rlt b2 2.

We prove the intermediate claim Hb1eq: b1 = eps_ 1.

An exact proof term for the current goal is (andEL (b1 = eps_ 1) (Rlt b2 2) Hc).

We prove the intermediate claim Hbad: Rlt (eps_ 1) (eps_ 1).

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

An exact proof term for the current goal is Hlt.

An exact proof term for the current goal is ((not_Rlt_refl (eps_ 1) Heps1R) Hbad).

Assume Hc: (eps_ 1) = b1 ∧ Rlt (eps_ 1) b2.

We prove the intermediate claim Heq: (eps_ 1) = b1.

An exact proof term for the current goal is (andEL ((eps_ 1) = b1) (Rlt (eps_ 1) b2) Hc).

We prove the intermediate claim Hltb2: Rlt (eps_ 1) b2.

An exact proof term for the current goal is (andER ((eps_ 1) = b1) (Rlt (eps_ 1) b2) Hc).

We prove the intermediate claim HpEq0: p = (eps_ 1,b2).

We will prove p = (eps_ 1,b2).

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

An exact proof term for the current goal is HpEq.

We prove the intermediate claim HpEq1: p = (eps_ 1,y).

We will prove p = (eps_ 1,y).

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

An exact proof term for the current goal is HpEq0.

We prove the intermediate claim Hylt: Rlt (eps_ 1) y.

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

An exact proof term for the current goal is Hltb2.

An exact proof term for the current goal is (andI (p = (eps_ 1,y)) (Rlt (eps_ 1) y) HpEq1 Hylt).

Apply andI to the current goal.

An exact proof term for the current goal is HpFirst.

An exact proof term for the current goal is Hyprop.

An exact proof term for the current goal is (SepI ordered_square (λp0 : set ⇒ ∃y : set, p0 = (eps_ 1,y) ∧ Rlt (eps_ 1) y ∧ ¬ (Rlt 1 y)) p HpSq Hexists).

We prove the intermediate claim Hex: ∃W ∈ R2_dictionary_order_topology, U = W ∩ ordered_square.

We use V to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HVTx.

An exact proof term for the current goal is HeqU.

An exact proof term for the current goal is (SepI (𝒫 ordered_square) (λU0 : set ⇒ ∃W ∈ R2_dictionary_order_topology, U0 = W ∩ ordered_square) U HUpow Hex).

We prove the intermediate claim HUprod: U ∈ Tprod.

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

An exact proof term for the current goal is HUdic.

We prove the intermediate claim HUnprod: ¬ (U ∈ Tprod).

Assume HUin: U ∈ Tprod.

Set p0 to be the term (eps_ 1,1).

We prove the intermediate claim Hp0U: p0 ∈ U.

We prove the intermediate claim H1omega: 1 ∈ ω.

An exact proof term for the current goal is (nat_p_omega 1 nat_1).

We prove the intermediate claim Heps1SNoS: eps_ 1 ∈ SNoS_ ω.

An exact proof term for the current goal is (SNo_eps_SNoS_omega 1 H1omega).

We prove the intermediate claim Heps1R: eps_ 1 ∈ R.

An exact proof term for the current goal is (SNoS_omega_real (eps_ 1) Heps1SNoS).

We prove the intermediate claim HdefR: R = real.

Use reflexivity.

We prove the intermediate claim H1R: 1 ∈ R.

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

An exact proof term for the current goal is real_1.

We prove the intermediate claim H0R: 0 ∈ R.

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

An exact proof term for the current goal is real_0.

We prove the intermediate claim H0in1: 0 ∈ 1.

We prove the intermediate claim H0Ord: ordinal 0.

An exact proof term for the current goal is (nat_p_ordinal 0 nat_0).

An exact proof term for the current goal is (ordinal_0_In_ordsucc 0 H0Ord).

We prove the intermediate claim Heps1lt1: eps_ 1 < 1.

We prove the intermediate claim Heps1ltE0: eps_ 1 < eps_ 0.

An exact proof term for the current goal is (SNo_eps_decr 1 H1omega 0 H0in1).

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

An exact proof term for the current goal is Heps1ltE0.

We prove the intermediate claim Heps1lt1R: Rlt (eps_ 1) 1.

An exact proof term for the current goal is (RltI (eps_ 1) 1 Heps1R H1R Heps1lt1).

We prove the intermediate claim H0lt1: Rlt 0 1.

An exact proof term for the current goal is (RltI 0 1 H0R H1R SNoLt_0_1).

We prove the intermediate claim H0lteps1: Rlt 0 (eps_ 1).

An exact proof term for the current goal is (RltI 0 (eps_ 1) H0R Heps1R (SNo_eps_pos 1 H1omega)).

We prove the intermediate claim Hnlt_eps10: ¬ (Rlt (eps_ 1) 0).

An exact proof term for the current goal is (not_Rlt_sym 0 (eps_ 1) H0lteps1).

We prove the intermediate claim Hnlt_1eps1: ¬ (Rlt 1 (eps_ 1)).

An exact proof term for the current goal is (not_Rlt_sym (eps_ 1) 1 Heps1lt1R).

We prove the intermediate claim Hnlt_10: ¬ (Rlt 1 0).

An exact proof term for the current goal is (not_Rlt_sym 0 1 H0lt1).

We prove the intermediate claim Hnlt_11: ¬ (Rlt 1 1).

An exact proof term for the current goal is (not_Rlt_refl 1 H1R).

We prove the intermediate claim Heps1U: (eps_ 1) ∈ unit_interval.

An exact proof term for the current goal is (SepI R (λt : set ⇒ ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t)) (eps_ 1) Heps1R (andI (¬ (Rlt (eps_ 1) 0)) (¬ (Rlt 1 (eps_ 1))) Hnlt_eps10 Hnlt_1eps1)).

We prove the intermediate claim H1U: 1 ∈ unit_interval.

An exact proof term for the current goal is (SepI R (λt : set ⇒ ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t)) 1 H1R (andI (¬ (Rlt 1 0)) (¬ (Rlt 1 1)) Hnlt_10 Hnlt_11)).

We prove the intermediate claim Hp0Sq: p0 ∈ ordered_square.

We will prove (eps_ 1,1) ∈ setprod unit_interval unit_interval.

An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma unit_interval unit_interval (eps_ 1) 1 Heps1U H1U).

We prove the intermediate claim Hp0Ex: ∃y : set, p0 = (eps_ 1,y) ∧ Rlt (eps_ 1) y ∧ ¬ (Rlt 1 y).

We use 1 to witness the existential quantifier.

We will prove p0 = (eps_ 1,1) ∧ Rlt (eps_ 1) 1 ∧ ¬ (Rlt 1 1).

Apply andI to the current goal.

Use reflexivity.

An exact proof term for the current goal is Heps1lt1R.

An exact proof term for the current goal is Hnlt_11.

An exact proof term for the current goal is (SepI ordered_square (λq : set ⇒ ∃y : set, q = (eps_ 1,y) ∧ Rlt (eps_ 1) y ∧ ¬ (Rlt 1 y)) p0 Hp0Sq Hp0Ex).

Set X1 to be the term setprod unit_interval unit_interval.

Set B1 to be the term product_subbasis unit_interval unit_interval_topology unit_interval unit_interval_topology.

We prove the intermediate claim HTdef: Tprod = generated_topology X1 B1.

Use reflexivity.

We prove the intermediate claim HUgen: U ∈ generated_topology X1 B1.

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

An exact proof term for the current goal is HUin.

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

An exact proof term for the current goal is (SepE2 (𝒫 X1) (λU0 : set ⇒ ∀x ∈ U0, ∃b ∈ B1, x ∈ b ∧ b ⊆ U0) U HUgen).

We prove the intermediate claim Href0: ∃b ∈ B1, p0 ∈ b ∧ b ⊆ U.

An exact proof term for the current goal is (Href p0 Hp0U).

Apply Href0 to the current goal.

Let b0 be given.

Assume Hb0pair.

Apply Hb0pair to the current goal.

Assume Hb0B: b0 ∈ B1.

Assume Hb0core: p0 ∈ b0 ∧ b0 ⊆ U.

We prove the intermediate claim Hp0b0: p0 ∈ b0.

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

We prove the intermediate claim Hb0subU: b0 ⊆ U.

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

Apply (famunionE unit_interval_topology (λU0 : set ⇒ {rectangle_set U0 V|V ∈ unit_interval_topology}) b0 Hb0B) to the current goal.

Let U0 be given.

Assume HU0pair.

Apply HU0pair to the current goal.

Assume HU0Tx: U0 ∈ unit_interval_topology.

Assume Hb0Repl: b0 ∈ {rectangle_set U0 V|V ∈ unit_interval_topology}.

Apply (ReplE unit_interval_topology (λV0 : set ⇒ rectangle_set U0 V0) b0 Hb0Repl) to the current goal.

Let V0 be given.

Assume HV0pair.

Apply HV0pair to the current goal.

Assume HV0Ty: V0 ∈ unit_interval_topology.

Assume Hb0eq: b0 = rectangle_set U0 V0.

We prove the intermediate claim Hp0rect: p0 ∈ rectangle_set U0 V0.

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

An exact proof term for the current goal is Hp0b0.

We prove the intermediate claim Hp00: p0 0 = eps_ 1.

We prove the intermediate claim Hp0def: p0 = (eps_ 1,1).

Use reflexivity.

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

An exact proof term for the current goal is (tuple_2_0_eq (eps_ 1) 1).

We prove the intermediate claim Hp01: p0 1 = 1.

We prove the intermediate claim Hp0def: p0 = (eps_ 1,1).

Use reflexivity.

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

An exact proof term for the current goal is (tuple_2_1_eq (eps_ 1) 1).

We prove the intermediate claim HepsU0: (eps_ 1) ∈ U0.

We prove the intermediate claim Hp0U0: (p0 0) ∈ U0.

An exact proof term for the current goal is (ap0_Sigma U0 (λ_ : set ⇒ V0) p0 Hp0rect).

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

An exact proof term for the current goal is Hp0U0.

We prove the intermediate claim H1V0: 1 ∈ V0.

We prove the intermediate claim Hp0V0: (p0 1) ∈ V0.

An exact proof term for the current goal is (ap1_Sigma U0 (λ_ : set ⇒ V0) p0 Hp0rect).

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

An exact proof term for the current goal is Hp0V0.

We prove the intermediate claim Hexother: ∃x : set, x ∈ U0 ∧ x ≠ eps_ 1.

An exact proof term for the current goal is (unit_interval_open_neighborhood_has_other_point U0 HU0Tx HepsU0).

Apply Hexother to the current goal.

Let x be given.

Assume Hxpair.

We prove the intermediate claim HxU0: x ∈ U0.

An exact proof term for the current goal is (andEL (x ∈ U0) (x ≠ eps_ 1) Hxpair).

We prove the intermediate claim Hxneq: x ≠ eps_ 1.

An exact proof term for the current goal is (andER (x ∈ U0) (x ≠ eps_ 1) Hxpair).

Set p1 to be the term (x,1).

We prove the intermediate claim Hp1b0: p1 ∈ b0.

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

We will prove p1 ∈ rectangle_set U0 V0.

An exact proof term for the current goal is (tuple_2_rectangle_set U0 V0 x 1 HxU0 H1V0).

We prove the intermediate claim Hp1U: p1 ∈ U.

An exact proof term for the current goal is (Hb0subU p1 Hp1b0).

We prove the intermediate claim Hstrip: ∃y : set, p1 = (eps_ 1,y) ∧ Rlt (eps_ 1) y ∧ ¬ (Rlt 1 y).

An exact proof term for the current goal is (SepE2 ordered_square (λq : set ⇒ ∃y : set, q = (eps_ 1,y) ∧ Rlt (eps_ 1) y ∧ ¬ (Rlt 1 y)) p1 Hp1U).

Apply Hstrip to the current goal.

Let y be given.

Assume Hyprop.

We prove the intermediate claim Hycore: p1 = (eps_ 1,y) ∧ Rlt (eps_ 1) y.

An exact proof term for the current goal is (andEL (p1 = (eps_ 1,y) ∧ Rlt (eps_ 1) y) (¬ (Rlt 1 y)) Hyprop).

We prove the intermediate claim HyPair: p1 = (eps_ 1,y).

An exact proof term for the current goal is (andEL (p1 = (eps_ 1,y)) (Rlt (eps_ 1) y) Hycore).

We prove the intermediate claim Hp10: p1 0 = x.

We prove the intermediate claim Hp1def: p1 = (x,1).

Use reflexivity.

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

An exact proof term for the current goal is (tuple_2_0_eq x 1).

We prove the intermediate claim Hp10': p1 0 = eps_ 1.

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

An exact proof term for the current goal is (tuple_2_0_eq (eps_ 1) y).

We prove the intermediate claim Hxeq: x = eps_ 1.

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

An exact proof term for the current goal is Hp10'.

Apply FalseE to the current goal.

An exact proof term for the current goal is (Hxneq Hxeq).

An exact proof term for the current goal is (HUnprod HUprod).