Let p be given.

Assume Hpcl: p ∈ closure_of ordered_square ordered_square_topology ordsq_B.

We will prove p ∈ ordsq_B ∪ {ordsq_p10}.

We prove the intermediate claim Hdefcl: closure_of ordered_square ordered_square_topology ordsq_B = {x ∈ ordered_square|∀U : set, U ∈ ordered_square_topology → x ∈ U → U ∩ ordsq_B ≠ Empty}.

Use reflexivity.

We prove the intermediate claim Hpcl': p ∈ {x ∈ ordered_square|∀U : set, U ∈ ordered_square_topology → x ∈ U → U ∩ ordsq_B ≠ Empty}.

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

An exact proof term for the current goal is Hpcl.

We prove the intermediate claim HpSq: p ∈ ordered_square.

An exact proof term for the current goal is (SepE1 ordered_square (λx0 : set ⇒ ∀U : set, U ∈ ordered_square_topology → x0 ∈ U → U ∩ ordsq_B ≠ Empty) p Hpcl').

We prove the intermediate claim Hcond: ∀U : set, U ∈ ordered_square_topology → p ∈ U → U ∩ ordsq_B ≠ Empty.

An exact proof term for the current goal is (SepE2 ordered_square (λx0 : set ⇒ ∀U : set, U ∈ ordered_square_topology → x0 ∈ U → U ∩ ordsq_B ≠ Empty) p Hpcl').

Apply (xm (p ∈ ordsq_B)) to the current goal.

Assume HpB: p ∈ ordsq_B.

An exact proof term for the current goal is (binunionI1 ordsq_B {ordsq_p10} p HpB).

Assume HpNotB: ¬ (p ∈ ordsq_B).

Apply binunionI2 to the current goal.

Set p10 to be the term ordsq_p10.

We prove the intermediate claim Hp10def: p10 = (1,0).

Use reflexivity.

We prove the intermediate claim Hp10Sq: p10 ∈ ordered_square.

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

An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma unit_interval unit_interval 1 0 one_in_unit_interval zero_in_unit_interval).

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

An exact proof term for the current goal is ((setprod_Subq unit_interval unit_interval R R unit_interval_sub_R unit_interval_sub_R) p HpSq).

We prove the intermediate claim Hp10RR: p10 ∈ setprod R R.

An exact proof term for the current goal is ((setprod_Subq unit_interval unit_interval R R unit_interval_sub_R unit_interval_sub_R) p10 Hp10Sq).

Set U0 to be the term {x0 ∈ ordered_square|order_rel (setprod R R) p10 x0}.

We prove the intermediate claim HU0Pow: U0 ∈ 𝒫 ordered_square.

An exact proof term for the current goal is (Sep_In_Power ordered_square (λx0 : set ⇒ order_rel (setprod R R) p10 x0)).

We prove the intermediate claim HU0basis: U0 ∈ ordered_square_order_basis.

Set Bint to be the term {I ∈ 𝒫 ordered_square|∃a0 ∈ ordered_square, ∃b0 ∈ ordered_square, I = {x0 ∈ ordered_square|order_rel (setprod R R) a0 x0 ∧ order_rel (setprod R R) x0 b0}}.

Set Blow to be the term {I ∈ 𝒫 ordered_square|∃b0 ∈ ordered_square, I = {x0 ∈ ordered_square|order_rel (setprod R R) x0 b0}}.

Set Bup to be the term {I ∈ 𝒫 ordered_square|∃a0 ∈ ordered_square, I = {x0 ∈ ordered_square|order_rel (setprod R R) a0 x0}}.

We prove the intermediate claim HdefB: ordered_square_order_basis = ((Bint ∪ Blow) ∪ Bup).

Use reflexivity.

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

Apply binunionI2 to the current goal.

We will prove U0 ∈ Bup.

Apply (SepI (𝒫 ordered_square) (λI : set ⇒ ∃a0 ∈ ordered_square, I = {x0 ∈ ordered_square|order_rel (setprod R R) a0 x0}) U0) to the current goal.

An exact proof term for the current goal is HU0Pow.

We use p10 to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Hp10Sq.

Use reflexivity.

We prove the intermediate claim HU0top: U0 ∈ ordered_square_topology.

We prove the intermediate claim HdefT: ordered_square_topology = generated_topology ordered_square ordered_square_order_basis.

Use reflexivity.

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

An exact proof term for the current goal is (generated_topology_contains_elem ordered_square ordered_square_order_basis U0 HU0Pow HU0basis).

Apply (order_rel_trichotomy_or_impred (setprod R R) p p10 simply_ordered_set_setprod_R_R HpRR Hp10RR (p ∈ {ordsq_p10})) to the current goal.

Assume Hpp10: order_rel (setprod R R) p p10.

Apply FalseE to the current goal.

We prove the intermediate claim Hexw: ∃w : set, w ∈ {x0 ∈ ordered_square|order_rel (setprod R R) p x0} ∧ w ∈ ordsq_B.

An exact proof term for the current goal is (ex17_18_p10_upper_basis_meets_B p HpSq Hpp10).

Apply Hexw to the current goal.

Let w be given.

Assume Hwpack.

We prove the intermediate claim HwSep: w ∈ {x0 ∈ ordered_square|order_rel (setprod R R) p x0}.

An exact proof term for the current goal is (andEL (w ∈ {x0 ∈ ordered_square|order_rel (setprod R R) p x0}) (w ∈ ordsq_B) Hwpack).

We prove the intermediate claim HwB: w ∈ ordsq_B.

An exact proof term for the current goal is (andER (w ∈ {x0 ∈ ordered_square|order_rel (setprod R R) p x0}) (w ∈ ordsq_B) Hwpack).

We prove the intermediate claim Hpw: order_rel (setprod R R) p w.

An exact proof term for the current goal is (SepE2 ordered_square (λx0 : set ⇒ order_rel (setprod R R) p x0) w HwSep).

We prove the intermediate claim Hexn: ∃n ∈ ω ∖ {0}, w = (add_SNo 1 (minus_SNo (inv_nat n)),eps_ 1).

An exact proof term for the current goal is (ReplE (ω ∖ {0}) (λn0 : set ⇒ (add_SNo 1 (minus_SNo (inv_nat n0)),eps_ 1)) w HwB).

Apply Hexn to the current goal.

Let n be given.

Assume Hnpack.

Apply Hnpack to the current goal.

Assume HnIn HwEq.

We prove the intermediate claim Hpn: order_rel (setprod R R) p (add_SNo 1 (minus_SNo (inv_nat n)),eps_ 1).

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

An exact proof term for the current goal is Hpw.

Set Pn to be the term (λn0 : set ⇒ n0 ∈ ω ∖ {0} ∧ order_rel (setprod R R) p (add_SNo 1 (minus_SNo (inv_nat n0)),eps_ 1)).

We prove the intermediate claim HexOrd: ∃alpha : set, ordinal alpha ∧ Pn alpha.

We use n to witness the existential quantifier.

We will prove ordinal n ∧ Pn n.

Apply andI to the current goal.

An exact proof term for the current goal is (ordinal_Hered ω omega_ordinal n (setminusE1 ω {0} n HnIn)).

We will prove n ∈ ω ∖ {0} ∧ order_rel (setprod R R) p (add_SNo 1 (minus_SNo (inv_nat n)),eps_ 1).

Apply andI to the current goal.

An exact proof term for the current goal is HnIn.

An exact proof term for the current goal is Hpn.

Apply (least_ordinal_ex Pn HexOrd) to the current goal.

Let nmin be given.

Assume HminPack.

We prove the intermediate claim Hmin12: (ordinal nmin ∧ Pn nmin).

An exact proof term for the current goal is (andEL (ordinal nmin ∧ Pn nmin) (∀beta ∈ nmin, ¬ Pn beta) HminPack).

We prove the intermediate claim HminPn: Pn nmin.

An exact proof term for the current goal is (andER (ordinal nmin) (Pn nmin) Hmin12).

We prove the intermediate claim HminMin: ∀beta ∈ nmin, ¬ Pn beta.

An exact proof term for the current goal is (andER (ordinal nmin ∧ Pn nmin) (∀beta ∈ nmin, ¬ Pn beta) HminPack).

Apply HminPn to the current goal.

Assume HnminIn Hppmin.

We prove the intermediate claim HnminO: nmin ∈ ω.

An exact proof term for the current goal is (setminusE1 ω {0} nmin HnminIn).

We prove the intermediate claim HnminNat: nat_p nmin.

An exact proof term for the current goal is (omega_nat_p nmin HnminO).

We prove the intermediate claim HnminCase: nmin = 0 ∨ ∃m : set, nat_p m ∧ nmin = ordsucc m.

An exact proof term for the current goal is (nat_inv nmin HnminNat).

Apply HnminCase to the current goal.

Assume Hnmin0: nmin = 0.

We prove the intermediate claim HnminIn0: nmin ∈ {0}.

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

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

We prove the intermediate claim HnminNot0: nmin ∉ {0}.

An exact proof term for the current goal is (setminusE2 ω {0} nmin HnminIn).

An exact proof term for the current goal is (HnminNot0 HnminIn0).

Assume Hexm: ∃m : set, nat_p m ∧ nmin = ordsucc m.

Apply Hexm to the current goal.

Let m be given.

Assume Hmconj.

We prove the intermediate claim HmNat: nat_p m.

An exact proof term for the current goal is (andEL (nat_p m) (nmin = ordsucc m) Hmconj).

We prove the intermediate claim HmEq: nmin = ordsucc m.

An exact proof term for the current goal is (andER (nat_p m) (nmin = ordsucc m) Hmconj).

Apply (xm (m = 0)) to the current goal.

Assume Hm0: m = 0.

Set bmin to be the term (add_SNo 1 (minus_SNo (inv_nat nmin)),eps_ 1).

Set Ubad to be the term {x0 ∈ ordered_square|order_rel (setprod R R) x0 bmin}.

We prove the intermediate claim HUbadPow: Ubad ∈ 𝒫 ordered_square.

An exact proof term for the current goal is (Sep_In_Power ordered_square (λx0 : set ⇒ order_rel (setprod R R) x0 bmin)).

We prove the intermediate claim HbminSq: bmin ∈ ordered_square.

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

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

An exact proof term for the current goal is (ordsq_B_sub_ordered_square (add_SNo 1 (minus_SNo (inv_nat 1)),eps_ 1) (ReplI (ω ∖ {0}) (λn0 : set ⇒ (add_SNo 1 (minus_SNo (inv_nat n0)),eps_ 1)) 1 (setminusI ω {0} 1 (nat_p_omega 1 nat_1) (λH10 : 1 ∈ {0} ⇒ neq_1_0 (SingE 0 1 H10))))).

We prove the intermediate claim HUbadBasis: Ubad ∈ ordered_square_order_basis.

Set Bint to be the term {I ∈ 𝒫 ordered_square|∃a0 ∈ ordered_square, ∃b0 ∈ ordered_square, I = {x0 ∈ ordered_square|order_rel (setprod R R) a0 x0 ∧ order_rel (setprod R R) x0 b0}}.

Set Blow to be the term {I ∈ 𝒫 ordered_square|∃b0 ∈ ordered_square, I = {x0 ∈ ordered_square|order_rel (setprod R R) x0 b0}}.

Set Bup to be the term {I ∈ 𝒫 ordered_square|∃a0 ∈ ordered_square, I = {x0 ∈ ordered_square|order_rel (setprod R R) a0 x0}}.

We prove the intermediate claim HdefB: ordered_square_order_basis = ((Bint ∪ Blow) ∪ Bup).

Use reflexivity.

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

Apply binunionI1 to the current goal.

Apply binunionI2 to the current goal.

Apply (SepI (𝒫 ordered_square) (λI : set ⇒ ∃b0 ∈ ordered_square, I = {x0 ∈ ordered_square|order_rel (setprod R R) x0 b0}) Ubad) to the current goal.

An exact proof term for the current goal is HUbadPow.

We use bmin to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HbminSq.

Use reflexivity.

We prove the intermediate claim HUbadTop: Ubad ∈ ordered_square_topology.

We prove the intermediate claim HdefT: ordered_square_topology = generated_topology ordered_square ordered_square_order_basis.

Use reflexivity.

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

An exact proof term for the current goal is (generated_topology_contains_elem ordered_square ordered_square_order_basis Ubad HUbadPow HUbadBasis).

We prove the intermediate claim HpUbad: p ∈ Ubad.

Apply (SepI ordered_square (λx0 : set ⇒ order_rel (setprod R R) x0 bmin) p HpSq) to the current goal.

An exact proof term for the current goal is Hppmin.

We prove the intermediate claim HcapNe: Ubad ∩ ordsq_B ≠ Empty.

An exact proof term for the current goal is (Hcond Ubad HUbadTop HpUbad).

We prove the intermediate claim HcapEmp: Ubad ∩ ordsq_B = Empty.

Apply set_ext to the current goal.

Let x be given.

Assume Hx: x ∈ Ubad ∩ ordsq_B.

We will prove x ∈ Empty.

Apply binintersectE Ubad ordsq_B x Hx to the current goal.

Assume HxUbad HxB.

Apply FalseE to the current goal.

We prove the intermediate claim Hxbmin: order_rel (setprod R R) x bmin.

An exact proof term for the current goal is (SepE2 ordered_square (λx0 : set ⇒ order_rel (setprod R R) x0 bmin) x HxUbad).

We prove the intermediate claim Hexn: ∃n ∈ ω ∖ {0}, x = (add_SNo 1 (minus_SNo (inv_nat n)),eps_ 1).

An exact proof term for the current goal is (ReplE (ω ∖ {0}) (λn0 : set ⇒ (add_SNo 1 (minus_SNo (inv_nat n0)),eps_ 1)) x HxB).

Apply Hexn to the current goal.

Let n be given.

Assume Hnpack.

Apply Hnpack to the current goal.

Assume HnInx HxEq.

We prove the intermediate claim HxSq: x ∈ ordered_square.

An exact proof term for the current goal is (ordsq_B_sub_ordered_square x HxB).

We prove the intermediate claim HxRR: x ∈ setprod R R.

An exact proof term for the current goal is ((setprod_Subq unit_interval unit_interval R R unit_interval_sub_R unit_interval_sub_R) x HxSq).

We prove the intermediate claim HbminRR: bmin ∈ setprod R R.

An exact proof term for the current goal is ((setprod_Subq unit_interval unit_interval R R unit_interval_sub_R unit_interval_sub_R) bmin HbminSq).

We prove the intermediate claim HnO: n ∈ ω.

An exact proof term for the current goal is (setminusE1 ω {0} n HnInx).

We prove the intermediate claim HnNat: nat_p n.

An exact proof term for the current goal is (omega_nat_p n HnO).

We prove the intermediate claim HnCase: n = 0 ∨ ∃k : set, nat_p k ∧ n = ordsucc k.

An exact proof term for the current goal is (nat_inv n HnNat).

Apply HnCase to the current goal.

Assume Hn0: n = 0.

We prove the intermediate claim HnIn0: n ∈ {0}.

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

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

We prove the intermediate claim HnNot0: n ∉ {0}.

An exact proof term for the current goal is (setminusE2 ω {0} n HnInx).

An exact proof term for the current goal is (HnNot0 HnIn0).

Assume Hexk: ∃k : set, nat_p k ∧ n = ordsucc k.

Apply Hexk to the current goal.

Let k be given.

Assume Hkconj.

We prove the intermediate claim HkNat: nat_p k.

An exact proof term for the current goal is (andEL (nat_p k) (n = ordsucc k) Hkconj).

We prove the intermediate claim HnEq: n = ordsucc k.

An exact proof term for the current goal is (andER (nat_p k) (n = ordsucc k) Hkconj).

Apply (xm (k = 0)) to the current goal.

Assume Hk0: k = 0.

We prove the intermediate claim HnEq1: n = nmin.

We prove the intermediate claim HnEq0: n = ordsucc 0.

We will prove n = ordsucc 0.

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

An exact proof term for the current goal is HnEq.

We prove the intermediate claim HnminEq0: nmin = ordsucc 0.

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

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

Use reflexivity.

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

An exact proof term for the current goal is HnEq0.

We prove the intermediate claim HxEqbmin: x = bmin.

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

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

Use reflexivity.

We prove the intermediate claim Hbb: order_rel (setprod R R) bmin bmin.

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

An exact proof term for the current goal is Hxbmin.

An exact proof term for the current goal is ((order_rel_irref (setprod R R) bmin) Hbb).

Assume HkNot0: ¬ (k = 0).

We prove the intermediate claim HkO: k ∈ ω.

An exact proof term for the current goal is (nat_p_omega k HkNat).

We prove the intermediate claim HkCase: k = 0 ∨ ∃t : set, nat_p t ∧ k = ordsucc t.

An exact proof term for the current goal is (nat_inv k HkNat).

Apply HkCase to the current goal.

Assume Hk0: k = 0.

An exact proof term for the current goal is (HkNot0 Hk0).

Assume Hext: ∃t : set, nat_p t ∧ k = ordsucc t.

Apply Hext to the current goal.

Let t be given.

Assume Htconj.

We prove the intermediate claim HtNat: nat_p t.

An exact proof term for the current goal is (andEL (nat_p t) (k = ordsucc t) Htconj).

We prove the intermediate claim HkEqS: k = ordsucc t.

An exact proof term for the current goal is (andER (nat_p t) (k = ordsucc t) Htconj).

We prove the intermediate claim H0ink: 0 ∈ k.

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

An exact proof term for the current goal is (nat_0_in_ordsucc t HtNat).

We prove the intermediate claim H0omega: 0 ∈ ω.

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

We prove the intermediate claim Hbminltx: order_rel (setprod R R) bmin x.

We prove the intermediate claim Htmp: order_rel (setprod R R) (add_SNo 1 (minus_SNo (inv_nat (ordsucc 0))),eps_ 1) (add_SNo 1 (minus_SNo (inv_nat (ordsucc k))),eps_ 1).

An exact proof term for the current goal is (ordsq_B_ordsucc_index_increasing 0 k H0omega HkO H0ink).

We prove the intermediate claim HbminEq: bmin = (add_SNo 1 (minus_SNo (inv_nat (ordsucc 0))),eps_ 1).

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

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

Use reflexivity.

We prove the intermediate claim HxEqk: x = (add_SNo 1 (minus_SNo (inv_nat (ordsucc k))),eps_ 1).

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

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

Use reflexivity.

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

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

An exact proof term for the current goal is Htmp.

We prove the intermediate claim Hxx: order_rel (setprod R R) x x.

An exact proof term for the current goal is (order_rel_trans (setprod R R) x bmin x simply_ordered_set_setprod_R_R HxRR HbminRR HxRR Hxbmin Hbminltx).

An exact proof term for the current goal is ((order_rel_irref (setprod R R) x) Hxx).

Let x be given.

Assume Hx: x ∈ Empty.

We will prove x ∈ Ubad ∩ ordsq_B.

Apply FalseE to the current goal.

An exact proof term for the current goal is (EmptyE x Hx).

Apply HcapNe to the current goal.

An exact proof term for the current goal is HcapEmp.

Assume HmNot0: ¬ (m = 0).

Apply FalseE to the current goal.

Set bprev to be the term (add_SNo 1 (minus_SNo (inv_nat m)),eps_ 1).

Set bcur to be the term (add_SNo 1 (minus_SNo (inv_nat nmin)),eps_ 1).

We prove the intermediate claim HmO: m ∈ ω.

An exact proof term for the current goal is (nat_p_omega m HmNat).

We prove the intermediate claim HmNotIn0: m ∉ {0}.

Assume HmIn0: m ∈ {0}.

We prove the intermediate claim Hm0: m = 0.

An exact proof term for the current goal is (SingE 0 m HmIn0).

An exact proof term for the current goal is (HmNot0 Hm0).

We prove the intermediate claim HmIn: m ∈ ω ∖ {0}.

An exact proof term for the current goal is (setminusI ω {0} m HmO HmNotIn0).

We prove the intermediate claim HbprevB: bprev ∈ ordsq_B.

An exact proof term for the current goal is (ReplI (ω ∖ {0}) (λn0 : set ⇒ (add_SNo 1 (minus_SNo (inv_nat n0)),eps_ 1)) m HmIn).

We prove the intermediate claim HbprevSq: bprev ∈ ordered_square.

An exact proof term for the current goal is (ordsq_B_sub_ordered_square bprev HbprevB).

We prove the intermediate claim HbprevRR: bprev ∈ setprod R R.

An exact proof term for the current goal is ((setprod_Subq unit_interval unit_interval R R unit_interval_sub_R unit_interval_sub_R) bprev HbprevSq).

We prove the intermediate claim HbcurSq: bcur ∈ ordered_square.

An exact proof term for the current goal is (ordsq_B_sub_ordered_square bcur (ReplI (ω ∖ {0}) (λn0 : set ⇒ (add_SNo 1 (minus_SNo (inv_nat n0)),eps_ 1)) nmin HnminIn)).

We prove the intermediate claim HbcurRR: bcur ∈ setprod R R.

An exact proof term for the current goal is ((setprod_Subq unit_interval unit_interval R R unit_interval_sub_R unit_interval_sub_R) bcur HbcurSq).

We prove the intermediate claim HmInNmin: m ∈ nmin.

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

An exact proof term for the current goal is (ordsuccI2 m).

We prove the intermediate claim HnotPnm: ¬ Pn m.

An exact proof term for the current goal is (HminMin m HmInNmin).

We prove the intermediate claim HnotPpm: ¬ (order_rel (setprod R R) p bprev).

Assume Hpprev: order_rel (setprod R R) p bprev.

We prove the intermediate claim HPn: Pn m.

We will prove m ∈ ω ∖ {0} ∧ order_rel (setprod R R) p bprev.

Apply andI to the current goal.

An exact proof term for the current goal is HmIn.

An exact proof term for the current goal is Hpprev.

An exact proof term for the current goal is (HnotPnm HPn).

We prove the intermediate claim Hbprevp: order_rel (setprod R R) bprev p.

Apply (order_rel_trichotomy_or_impred (setprod R R) p bprev simply_ordered_set_setprod_R_R HpRR HbprevRR (order_rel (setprod R R) bprev p)) to the current goal.

Assume Hpprev: order_rel (setprod R R) p bprev.

Apply FalseE to the current goal.

An exact proof term for the current goal is (HnotPpm Hpprev).

Assume HpEq: p = bprev.

Apply FalseE to the current goal.

We prove the intermediate claim HpB: p ∈ ordsq_B.

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

An exact proof term for the current goal is HbprevB.

An exact proof term for the current goal is (HpNotB HpB).

Assume Hbprevp0: order_rel (setprod R R) bprev p.

An exact proof term for the current goal is Hbprevp0.

Set Ugap to be the term {x0 ∈ ordered_square|order_rel (setprod R R) bprev x0 ∧ order_rel (setprod R R) x0 bcur}.

We prove the intermediate claim HUgapPow: Ugap ∈ 𝒫 ordered_square.

An exact proof term for the current goal is (Sep_In_Power ordered_square (λx0 : set ⇒ order_rel (setprod R R) bprev x0 ∧ order_rel (setprod R R) x0 bcur)).

We prove the intermediate claim HUgapBasis: Ugap ∈ ordered_square_order_basis.

Set Bint to be the term {I ∈ 𝒫 ordered_square|∃a0 ∈ ordered_square, ∃b0 ∈ ordered_square, I = {x0 ∈ ordered_square|order_rel (setprod R R) a0 x0 ∧ order_rel (setprod R R) x0 b0}}.

Set Blow to be the term {I ∈ 𝒫 ordered_square|∃b0 ∈ ordered_square, I = {x0 ∈ ordered_square|order_rel (setprod R R) x0 b0}}.

Set Bup to be the term {I ∈ 𝒫 ordered_square|∃a0 ∈ ordered_square, I = {x0 ∈ ordered_square|order_rel (setprod R R) a0 x0}}.

We prove the intermediate claim HdefB: ordered_square_order_basis = ((Bint ∪ Blow) ∪ Bup).

Use reflexivity.

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

Apply binunionI1 to the current goal.

Apply (SepI (𝒫 ordered_square) (λI : set ⇒ ∃a0 ∈ ordered_square, ∃b0 ∈ ordered_square, I = {x0 ∈ ordered_square|order_rel (setprod R R) a0 x0 ∧ order_rel (setprod R R) x0 b0}) Ugap) to the current goal.

An exact proof term for the current goal is HUgapPow.

We use bprev to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HbprevSq.

We use bcur to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HbcurSq.

Use reflexivity.

We prove the intermediate claim HUgapTop: Ugap ∈ ordered_square_topology.

We prove the intermediate claim HdefT: ordered_square_topology = generated_topology ordered_square ordered_square_order_basis.

Use reflexivity.

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

An exact proof term for the current goal is (generated_topology_contains_elem ordered_square ordered_square_order_basis Ugap HUgapPow HUgapBasis).

We prove the intermediate claim HpUgap: p ∈ Ugap.

Apply (SepI ordered_square (λx0 : set ⇒ order_rel (setprod R R) bprev x0 ∧ order_rel (setprod R R) x0 bcur) p HpSq) to the current goal.

Apply andI to the current goal.

An exact proof term for the current goal is Hbprevp.

An exact proof term for the current goal is Hppmin.

We prove the intermediate claim HcapNe2: Ugap ∩ ordsq_B ≠ Empty.

An exact proof term for the current goal is (Hcond Ugap HUgapTop HpUgap).

We prove the intermediate claim HcapEmp2: Ugap ∩ ordsq_B = Empty.

Apply set_ext to the current goal.

Let x be given.

Assume Hx: x ∈ Ugap ∩ ordsq_B.

We will prove x ∈ Empty.

Apply FalseE to the current goal.

Apply binintersectE Ugap ordsq_B x Hx to the current goal.

Assume HxGap HxB.

We prove the intermediate claim HxGapProp: order_rel (setprod R R) bprev x ∧ order_rel (setprod R R) x bcur.

An exact proof term for the current goal is (SepE2 ordered_square (λx0 : set ⇒ order_rel (setprod R R) bprev x0 ∧ order_rel (setprod R R) x0 bcur) x HxGap).

We prove the intermediate claim Hbprevx: order_rel (setprod R R) bprev x.

An exact proof term for the current goal is (andEL (order_rel (setprod R R) bprev x) (order_rel (setprod R R) x bcur) HxGapProp).

We prove the intermediate claim Hxbcur: order_rel (setprod R R) x bcur.

An exact proof term for the current goal is (andER (order_rel (setprod R R) bprev x) (order_rel (setprod R R) x bcur) HxGapProp).

We prove the intermediate claim Hexn: ∃n ∈ ω ∖ {0}, x = (add_SNo 1 (minus_SNo (inv_nat n)),eps_ 1).

An exact proof term for the current goal is (ReplE (ω ∖ {0}) (λn0 : set ⇒ (add_SNo 1 (minus_SNo (inv_nat n0)),eps_ 1)) x HxB).

Apply Hexn to the current goal.

Let n be given.

Assume Hnpack.

Apply Hnpack to the current goal.

Assume HnIn HxEq.

We prove the intermediate claim HnO: n ∈ ω.

An exact proof term for the current goal is (setminusE1 ω {0} n HnIn).

We prove the intermediate claim HnNat: nat_p n.

An exact proof term for the current goal is (omega_nat_p n HnO).

We prove the intermediate claim HnCase: n = 0 ∨ ∃j : set, nat_p j ∧ n = ordsucc j.

An exact proof term for the current goal is (nat_inv n HnNat).

Apply HnCase to the current goal.

Assume Hn0: n = 0.

We prove the intermediate claim HnIn0: n ∈ {0}.

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

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

We prove the intermediate claim HnNot0: n ∉ {0}.

An exact proof term for the current goal is (setminusE2 ω {0} n HnIn).

An exact proof term for the current goal is (HnNot0 HnIn0).

Assume Hexj: ∃j : set, nat_p j ∧ n = ordsucc j.

Apply Hexj to the current goal.

Let j be given.

Assume Hjconj.

We prove the intermediate claim HjNat: nat_p j.

An exact proof term for the current goal is (andEL (nat_p j) (n = ordsucc j) Hjconj).

We prove the intermediate claim HnEq: n = ordsucc j.

An exact proof term for the current goal is (andER (nat_p j) (n = ordsucc j) Hjconj).

We prove the intermediate claim HjO: j ∈ ω.

An exact proof term for the current goal is (nat_p_omega j HjNat).

We prove the intermediate claim HjOrd: ordinal j.

An exact proof term for the current goal is (nat_p_ordinal j HjNat).

We prove the intermediate claim HmCase: m = 0 ∨ ∃i : set, nat_p i ∧ m = ordsucc i.

An exact proof term for the current goal is (nat_inv m HmNat).

Apply HmCase to the current goal.

Assume Hm0: m = 0.

An exact proof term for the current goal is (HmNot0 Hm0).

Assume Hexi: ∃i : set, nat_p i ∧ m = ordsucc i.

Apply Hexi to the current goal.

Let i be given.

Assume Hiconj.

We prove the intermediate claim HiNat: nat_p i.

An exact proof term for the current goal is (andEL (nat_p i) (m = ordsucc i) Hiconj).

We prove the intermediate claim HmEqI: m = ordsucc i.

An exact proof term for the current goal is (andER (nat_p i) (m = ordsucc i) Hiconj).

We prove the intermediate claim HiO: i ∈ ω.

An exact proof term for the current goal is (nat_p_omega i HiNat).

We prove the intermediate claim HiOrd: ordinal i.

An exact proof term for the current goal is (nat_p_ordinal i HiNat).

We prove the intermediate claim HsuccIO: ordsucc i ∈ ω.

An exact proof term for the current goal is (omega_ordsucc i HiO).

We prove the intermediate claim HsuccIOrd: ordinal (ordsucc i).

An exact proof term for the current goal is (ordinal_Hered ω omega_ordinal (ordsucc i) HsuccIO).

We prove the intermediate claim HbprevEq: bprev = (add_SNo 1 (minus_SNo (inv_nat (ordsucc i))),eps_ 1).

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

Use reflexivity.

We prove the intermediate claim HxEqJ: x = (add_SNo 1 (minus_SNo (inv_nat (ordsucc j))),eps_ 1).

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

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

Use reflexivity.

We prove the intermediate claim HbcurEq: bcur = (add_SNo 1 (minus_SNo (inv_nat (ordsucc (ordsucc i)))),eps_ 1).

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

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

Use reflexivity.

We prove the intermediate claim Hlt_ij: order_rel (setprod R R) (add_SNo 1 (minus_SNo (inv_nat (ordsucc i))),eps_ 1) (add_SNo 1 (minus_SNo (inv_nat (ordsucc j))),eps_ 1).

We will prove order_rel (setprod R R) (add_SNo 1 (minus_SNo (inv_nat (ordsucc i))),eps_ 1) (add_SNo 1 (minus_SNo (inv_nat (ordsucc j))),eps_ 1).

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

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

An exact proof term for the current goal is Hbprevx.

We prove the intermediate claim HiInj: i ∈ j.

Apply (ordinal_trichotomy_or_impred i j HiOrd HjOrd (i ∈ j)) to the current goal.

Assume Hij: i ∈ j.

An exact proof term for the current goal is Hij.

Assume Hieq: i = j.

Apply FalseE to the current goal.

We prove the intermediate claim Hbad: order_rel (setprod R R) (add_SNo 1 (minus_SNo (inv_nat (ordsucc i))),eps_ 1) (add_SNo 1 (minus_SNo (inv_nat (ordsucc i))),eps_ 1).

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

An exact proof term for the current goal is Hlt_ij.

An exact proof term for the current goal is ((order_rel_irref (setprod R R) (add_SNo 1 (minus_SNo (inv_nat (ordsucc i))),eps_ 1)) Hbad).

Assume Hji: j ∈ i.

Apply FalseE to the current goal.

We prove the intermediate claim Hlt_ji: order_rel (setprod R R) (add_SNo 1 (minus_SNo (inv_nat (ordsucc j))),eps_ 1) (add_SNo 1 (minus_SNo (inv_nat (ordsucc i))),eps_ 1).

An exact proof term for the current goal is (ordsq_B_ordsucc_index_increasing j i HjO HiO Hji).

We prove the intermediate claim Hxx: order_rel (setprod R R) (add_SNo 1 (minus_SNo (inv_nat (ordsucc j))),eps_ 1) (add_SNo 1 (minus_SNo (inv_nat (ordsucc j))),eps_ 1).

An exact proof term for the current goal is ((order_rel_irref (setprod R R) (add_SNo 1 (minus_SNo (inv_nat (ordsucc j))),eps_ 1)) Hxx).

We prove the intermediate claim Hlt_j_succi: order_rel (setprod R R) (add_SNo 1 (minus_SNo (inv_nat (ordsucc j))),eps_ 1) (add_SNo 1 (minus_SNo (inv_nat (ordsucc (ordsucc i)))),eps_ 1).

We will prove order_rel (setprod R R) (add_SNo 1 (minus_SNo (inv_nat (ordsucc j))),eps_ 1) (add_SNo 1 (minus_SNo (inv_nat (ordsucc (ordsucc i)))),eps_ 1).

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

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

An exact proof term for the current goal is Hxbcur.

Apply (ordinal_trichotomy_or_impred j (ordsucc i) HjOrd HsuccIOrd False) to the current goal.

Assume HjIn: j ∈ ordsucc i.

Apply (ordsuccE i j HjIn) to the current goal.

Assume Hji: j ∈ i.

An exact proof term for the current goal is (In_no2cycle i j HiInj Hji).

Assume Hjeq: j = i.

We prove the intermediate claim Hii: i ∈ i.

We will prove i ∈ i.

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

An exact proof term for the current goal is HiInj.

An exact proof term for the current goal is (In_irref i Hii).

Assume Hjeq: j = ordsucc i.

Apply FalseE to the current goal.

We prove the intermediate claim HnEqSS: n = ordsucc (ordsucc i).

We will prove n = ordsucc (ordsucc i).

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

An exact proof term for the current goal is HnEq.

We prove the intermediate claim HnminEqSS: nmin = ordsucc (ordsucc i).

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

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

Use reflexivity.

We prove the intermediate claim HnEqNmin: n = nmin.

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

An exact proof term for the current goal is HnEqSS.

We prove the intermediate claim HxEqCur: x = bcur.

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

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

Use reflexivity.

We prove the intermediate claim Hbad: order_rel (setprod R R) bcur bcur.

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

An exact proof term for the current goal is Hxbcur.

An exact proof term for the current goal is ((order_rel_irref (setprod R R) bcur) Hbad).

Assume HsuccInj: ordsucc i ∈ j.

Apply FalseE to the current goal.

We prove the intermediate claim HsuccIO': ordsucc i ∈ ω.

An exact proof term for the current goal is HsuccIO.

We prove the intermediate claim Hlt_succi_j: order_rel (setprod R R) (add_SNo 1 (minus_SNo (inv_nat (ordsucc (ordsucc i)))),eps_ 1) (add_SNo 1 (minus_SNo (inv_nat (ordsucc j))),eps_ 1).

An exact proof term for the current goal is (ordsq_B_ordsucc_index_increasing (ordsucc i) j HsuccIO' HjO HsuccInj).

We prove the intermediate claim Hxx: order_rel (setprod R R) (add_SNo 1 (minus_SNo (inv_nat (ordsucc j))),eps_ 1) (add_SNo 1 (minus_SNo (inv_nat (ordsucc j))),eps_ 1).

An exact proof term for the current goal is ((order_rel_irref (setprod R R) (add_SNo 1 (minus_SNo (inv_nat (ordsucc j))),eps_ 1)) Hxx).

Let x be given.

Assume Hx: x ∈ Empty.

We will prove x ∈ Ugap ∩ ordsq_B.

Apply FalseE to the current goal.

An exact proof term for the current goal is (EmptyE x Hx).

Apply HcapNe2 to the current goal.

An exact proof term for the current goal is HcapEmp2.

Assume HpEq: p = p10.

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

An exact proof term for the current goal is (SingI ordsq_p10).

Assume Hp10p: order_rel (setprod R R) p10 p.

Apply FalseE to the current goal.

We prove the intermediate claim HpU0: p ∈ U0.

Apply (SepI ordered_square (λx0 : set ⇒ order_rel (setprod R R) p10 x0) p HpSq) to the current goal.

An exact proof term for the current goal is Hp10p.

We prove the intermediate claim HcapNe: U0 ∩ ordsq_B ≠ Empty.

An exact proof term for the current goal is (Hcond U0 HU0top HpU0).

We prove the intermediate claim Hexw: ∃w : set, w ∈ U0 ∩ ordsq_B.

An exact proof term for the current goal is (nonempty_has_element (U0 ∩ ordsq_B) HcapNe).

Apply Hexw to the current goal.

Let w be given.

Assume Hwcap.

We prove the intermediate claim HwU0: w ∈ U0.

An exact proof term for the current goal is (binintersectE1 U0 ordsq_B w Hwcap).

We prove the intermediate claim HwB: w ∈ ordsq_B.

An exact proof term for the current goal is (binintersectE2 U0 ordsq_B w Hwcap).

We prove the intermediate claim Hp10w: order_rel (setprod R R) p10 w.

An exact proof term for the current goal is (SepE2 ordered_square (λx0 : set ⇒ order_rel (setprod R R) p10 x0) w HwU0).

We prove the intermediate claim Hwp10: order_rel (setprod R R) w p10.

An exact proof term for the current goal is (ordsq_B_lt_p10 w HwB).

We prove the intermediate claim HwRR: w ∈ setprod R R.

We prove the intermediate claim HwSq: w ∈ ordered_square.

An exact proof term for the current goal is (SepE1 ordered_square (λx0 : set ⇒ order_rel (setprod R R) p10 x0) w HwU0).

An exact proof term for the current goal is ((setprod_Subq unit_interval unit_interval R R unit_interval_sub_R unit_interval_sub_R) w HwSq).

We prove the intermediate claim Hww: order_rel (setprod R R) w w.

An exact proof term for the current goal is (order_rel_trans (setprod R R) w p10 w simply_ordered_set_setprod_R_R HwRR Hp10RR HwRR Hwp10 Hp10w).

An exact proof term for the current goal is ((order_rel_irref (setprod R R) w) Hww).

Let p be given.

Assume Hp: p ∈ ordsq_B ∪ {ordsq_p10}.

We will prove p ∈ closure_of ordered_square ordered_square_topology ordsq_B.

Apply (binunionE ordsq_B {ordsq_p10} p Hp) to the current goal.

Assume HpB: p ∈ ordsq_B.

We prove the intermediate claim HpSq: p ∈ ordered_square.

An exact proof term for the current goal is (ordsq_B_sub_ordered_square p HpB).

Use reflexivity.

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

Apply (SepI ordered_square (λx0 : set ⇒ ∀U : set, U ∈ ordered_square_topology → x0 ∈ U → U ∩ ordsq_B ≠ Empty) p HpSq) to the current goal.

Let U be given.

Assume HUtop: U ∈ ordered_square_topology.

Assume HpU: p ∈ U.

We will prove U ∩ ordsq_B ≠ Empty.

We prove the intermediate claim HpUB: p ∈ U ∩ ordsq_B.

An exact proof term for the current goal is (binintersectI U ordsq_B p HpU HpB).

An exact proof term for the current goal is (elem_implies_nonempty (U ∩ ordsq_B) p HpUB).

Assume Hp10: p ∈ {ordsq_p10}.

We prove the intermediate claim HpEq: p = ordsq_p10.

An exact proof term for the current goal is (SingE ordsq_p10 p Hp10).

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

Set p10 to be the term ordsq_p10.

We prove the intermediate claim Hp10def: p10 = (1,0).

Use reflexivity.

We prove the intermediate claim Hp10Sq: p10 ∈ ordered_square.

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

An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma unit_interval unit_interval 1 0 one_in_unit_interval zero_in_unit_interval).

Use reflexivity.

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

Apply (SepI ordered_square (λx0 : set ⇒ ∀U : set, U ∈ ordered_square_topology → x0 ∈ U → U ∩ ordsq_B ≠ Empty) p10 Hp10Sq) to the current goal.

Let U be given.

Assume HUtop: U ∈ ordered_square_topology.

Assume Hp10U: p10 ∈ U.

We will prove U ∩ ordsq_B ≠ Empty.

We prove the intermediate claim HUgt: U ∈ generated_topology ordered_square ordered_square_order_basis.

We prove the intermediate claim HdefT: ordered_square_topology = generated_topology ordered_square ordered_square_order_basis.

Use reflexivity.

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

An exact proof term for the current goal is HUtop.

We prove the intermediate claim HexI: ∃I ∈ ordered_square_order_basis, p10 ∈ I ∧ I ⊆ U.

An exact proof term for the current goal is (generated_topology_local_refine ordered_square ordered_square_order_basis U p10 HUgt Hp10U).

Apply HexI to the current goal.

Let I be given.

Assume HIprop.

Apply HIprop to the current goal.

Assume HIbas HIcore.

Apply HIcore to the current goal.

Assume Hp10I HIU.

Set Bint to be the term {J ∈ 𝒫 ordered_square|∃a0 ∈ ordered_square, ∃b0 ∈ ordered_square, J = {x0 ∈ ordered_square|order_rel (setprod R R) a0 x0 ∧ order_rel (setprod R R) x0 b0}}.

Set Blow to be the term {J ∈ 𝒫 ordered_square|∃b0 ∈ ordered_square, J = {x0 ∈ ordered_square|order_rel (setprod R R) x0 b0}}.

Set Bup to be the term {J ∈ 𝒫 ordered_square|∃a0 ∈ ordered_square, J = {x0 ∈ ordered_square|order_rel (setprod R R) a0 x0}}.

We prove the intermediate claim HIcase: I ∈ ((Bint ∪ Blow) ∪ Bup).

We prove the intermediate claim HdefB: ordered_square_order_basis = ((Bint ∪ Blow) ∪ Bup).

Use reflexivity.

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

An exact proof term for the current goal is HIbas.

Apply (binunionE (Bint ∪ Blow) Bup I HIcase) to the current goal.

Assume HIin: I ∈ Bint ∪ Blow.

Apply (binunionE Bint Blow I HIin) to the current goal.

Assume HIint: I ∈ Bint.

We prove the intermediate claim Hexab: ∃a0 ∈ ordered_square, ∃b0 ∈ ordered_square, I = {x0 ∈ ordered_square|order_rel (setprod R R) a0 x0 ∧ order_rel (setprod R R) x0 b0}.

An exact proof term for the current goal is (SepE2 (𝒫 ordered_square) (λJ0 : set ⇒ ∃a0 ∈ ordered_square, ∃b0 ∈ ordered_square, J0 = {x0 ∈ ordered_square|order_rel (setprod R R) a0 x0 ∧ order_rel (setprod R R) x0 b0}) I HIint).

Apply Hexab to the current goal.

Let a0 be given.

Assume Ha0pack.

Apply Ha0pack to the current goal.

Assume Ha0Sq Hrest.

Apply Hrest to the current goal.

Let b0 be given.

Assume Hb0pack.

Apply Hb0pack to the current goal.

Assume Hb0Sq HIeq.

We prove the intermediate claim Hp10I': p10 ∈ {x0 ∈ ordered_square|order_rel (setprod R R) a0 x0 ∧ order_rel (setprod R R) x0 b0}.

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

An exact proof term for the current goal is Hp10I.

We prove the intermediate claim Hp10ord: order_rel (setprod R R) a0 p10 ∧ order_rel (setprod R R) p10 b0.

An exact proof term for the current goal is (SepE2 ordered_square (λx0 : set ⇒ order_rel (setprod R R) a0 x0 ∧ order_rel (setprod R R) x0 b0) p10 Hp10I').

We prove the intermediate claim Ha0p10: order_rel (setprod R R) a0 p10.

An exact proof term for the current goal is (andEL (order_rel (setprod R R) a0 p10) (order_rel (setprod R R) p10 b0) Hp10ord).

We prove the intermediate claim Hp10b0: order_rel (setprod R R) p10 b0.

An exact proof term for the current goal is (andER (order_rel (setprod R R) a0 p10) (order_rel (setprod R R) p10 b0) Hp10ord).

We prove the intermediate claim Hexw: ∃w : set, w ∈ {x0 ∈ ordered_square|order_rel (setprod R R) a0 x0 ∧ order_rel (setprod R R) x0 b0} ∧ w ∈ ordsq_B.

An exact proof term for the current goal is (ex17_18_p10_interval_basis_meets_B a0 b0 Ha0Sq Hb0Sq Ha0p10 Hp10b0).

Apply Hexw to the current goal.

Let w be given.

Assume Hwpack.

We prove the intermediate claim HwIset: w ∈ {x0 ∈ ordered_square|order_rel (setprod R R) a0 x0 ∧ order_rel (setprod R R) x0 b0}.

An exact proof term for the current goal is (andEL (w ∈ {x0 ∈ ordered_square|order_rel (setprod R R) a0 x0 ∧ order_rel (setprod R R) x0 b0}) (w ∈ ordsq_B) Hwpack).

We prove the intermediate claim HwB: w ∈ ordsq_B.

An exact proof term for the current goal is (andER (w ∈ {x0 ∈ ordered_square|order_rel (setprod R R) a0 x0 ∧ order_rel (setprod R R) x0 b0}) (w ∈ ordsq_B) Hwpack).

We prove the intermediate claim HwI: w ∈ I.

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

An exact proof term for the current goal is HwIset.

We prove the intermediate claim HwU: w ∈ U.

An exact proof term for the current goal is (HIU w HwI).

We prove the intermediate claim Hwcap: w ∈ U ∩ ordsq_B.

An exact proof term for the current goal is (binintersectI U ordsq_B w HwU HwB).

An exact proof term for the current goal is (elem_implies_nonempty (U ∩ ordsq_B) w Hwcap).

Assume HIlow: I ∈ Blow.

We prove the intermediate claim Hexb: ∃b0 ∈ ordered_square, I = {x0 ∈ ordered_square|order_rel (setprod R R) x0 b0}.

An exact proof term for the current goal is (SepE2 (𝒫 ordered_square) (λJ0 : set ⇒ ∃b0 ∈ ordered_square, J0 = {x0 ∈ ordered_square|order_rel (setprod R R) x0 b0}) I HIlow).

Apply Hexb to the current goal.

Let b0 be given.

Assume Hb0pack.

Apply Hb0pack to the current goal.

Assume Hb0Sq HIeq.

We prove the intermediate claim Hp10I': p10 ∈ {x0 ∈ ordered_square|order_rel (setprod R R) x0 b0}.

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

An exact proof term for the current goal is Hp10I.

We prove the intermediate claim Hp10b0: order_rel (setprod R R) p10 b0.

An exact proof term for the current goal is (SepE2 ordered_square (λx0 : set ⇒ order_rel (setprod R R) x0 b0) p10 Hp10I').

We prove the intermediate claim Hexw: ∃w : set, w ∈ {x0 ∈ ordered_square|order_rel (setprod R R) x0 b0} ∧ w ∈ ordsq_B.

An exact proof term for the current goal is (ex17_18_p10_lower_basis_meets_B b0 Hb0Sq Hp10b0).

Apply Hexw to the current goal.

Let w be given.

Assume Hwpack.

We prove the intermediate claim HwIset: w ∈ {x0 ∈ ordered_square|order_rel (setprod R R) x0 b0}.

An exact proof term for the current goal is (andEL (w ∈ {x0 ∈ ordered_square|order_rel (setprod R R) x0 b0}) (w ∈ ordsq_B) Hwpack).

We prove the intermediate claim HwB: w ∈ ordsq_B.

An exact proof term for the current goal is (andER (w ∈ {x0 ∈ ordered_square|order_rel (setprod R R) x0 b0}) (w ∈ ordsq_B) Hwpack).

We prove the intermediate claim HwI: w ∈ I.

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

An exact proof term for the current goal is HwIset.

We prove the intermediate claim HwU: w ∈ U.

An exact proof term for the current goal is (HIU w HwI).

We prove the intermediate claim Hwcap: w ∈ U ∩ ordsq_B.

An exact proof term for the current goal is (binintersectI U ordsq_B w HwU HwB).

An exact proof term for the current goal is (elem_implies_nonempty (U ∩ ordsq_B) w Hwcap).

Assume HIup: I ∈ Bup.

We prove the intermediate claim Hexa: ∃a0 ∈ ordered_square, I = {x0 ∈ ordered_square|order_rel (setprod R R) a0 x0}.

An exact proof term for the current goal is (SepE2 (𝒫 ordered_square) (λJ0 : set ⇒ ∃a0 ∈ ordered_square, J0 = {x0 ∈ ordered_square|order_rel (setprod R R) a0 x0}) I HIup).

Apply Hexa to the current goal.

Let a0 be given.

Assume Ha0pack.

Apply Ha0pack to the current goal.

Assume Ha0Sq HIeq.

We prove the intermediate claim Hp10I': p10 ∈ {x0 ∈ ordered_square|order_rel (setprod R R) a0 x0}.

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

An exact proof term for the current goal is Hp10I.

We prove the intermediate claim Ha0p10: order_rel (setprod R R) a0 p10.

An exact proof term for the current goal is (SepE2 ordered_square (λx0 : set ⇒ order_rel (setprod R R) a0 x0) p10 Hp10I').

We prove the intermediate claim Hexw: ∃w : set, w ∈ {x0 ∈ ordered_square|order_rel (setprod R R) a0 x0} ∧ w ∈ ordsq_B.

An exact proof term for the current goal is (ex17_18_p10_upper_basis_meets_B a0 Ha0Sq Ha0p10).

Apply Hexw to the current goal.

Let w be given.

Assume Hwpack.

We prove the intermediate claim HwIset: w ∈ {x0 ∈ ordered_square|order_rel (setprod R R) a0 x0}.

An exact proof term for the current goal is (andEL (w ∈ {x0 ∈ ordered_square|order_rel (setprod R R) a0 x0}) (w ∈ ordsq_B) Hwpack).

We prove the intermediate claim HwB: w ∈ ordsq_B.

An exact proof term for the current goal is (andER (w ∈ {x0 ∈ ordered_square|order_rel (setprod R R) a0 x0}) (w ∈ ordsq_B) Hwpack).

We prove the intermediate claim HwI: w ∈ I.

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

An exact proof term for the current goal is HwIset.

We prove the intermediate claim HwU: w ∈ U.

An exact proof term for the current goal is (HIU w HwI).

We prove the intermediate claim Hwcap: w ∈ U ∩ ordsq_B.

An exact proof term for the current goal is (binintersectI U ordsq_B w HwU HwB).

An exact proof term for the current goal is (elem_implies_nonempty (U ∩ ordsq_B) w Hwcap).