Let X and Tx be given.
Assume Hlin: linear_continuum X Tx.
We will prove normal_space X Tx.
Set T0 to be the term (simply_ordered_set X ∧ Tx = order_topology X) ∧ (∃x y : set, x ∈ X ∧ y ∈ X ∧ x ≠ y).
Set T1 to be the term T0 ∧ (∀x y : set, x ∈ X → y ∈ X → order_rel X x y → ∃z : set, z ∈ X ∧ order_rel X x z ∧ order_rel X z y).
Set T2 to be the term T1 ∧ (∀A : set, A ⊆ X → A ≠ Empty → (∃upper : set, upper ∈ X ∧ ∀a : set, a ∈ A → order_rel X a upper ∨ a = upper) → ∃lub : set, lub ∈ X ∧ (∀a : set, a ∈ A → order_rel X a lub ∨ a = lub) ∧ (∀bound : set, bound ∈ X → (∀a : set, a ∈ A → order_rel X a bound ∨ a = bound) → order_rel X lub bound ∨ lub = bound)).
We prove the intermediate claim HT2: T2.
An exact proof term for the current goal is Hlin.
We prove the intermediate claim HT1: T1.
An exact proof term for the current goal is (andEL T1 (∀A : set, A ⊆ X → A ≠ Empty → (∃upper : set, upper ∈ X ∧ ∀a : set, a ∈ A → order_rel X a upper ∨ a = upper) → ∃lub : set, lub ∈ X ∧ (∀a : set, a ∈ A → order_rel X a lub ∨ a = lub) ∧ (∀bound : set, bound ∈ X → (∀a : set, a ∈ A → order_rel X a bound ∨ a = bound) → order_rel X lub bound ∨ lub = bound)) HT2).
We prove the intermediate claim Hlub: ∀A : set, A ⊆ X → A ≠ Empty → (∃upper : set, upper ∈ X ∧ ∀a : set, a ∈ A → order_rel X a upper ∨ a = upper) → ∃lub : set, lub ∈ X ∧ (∀a : set, a ∈ A → order_rel X a lub ∨ a = lub) ∧ (∀bound : set, bound ∈ X → (∀a : set, a ∈ A → order_rel X a bound ∨ a = bound) → order_rel X lub bound ∨ lub = bound).
An exact proof term for the current goal is (andER T1 (∀A : set, A ⊆ X → A ≠ Empty → (∃upper : set, upper ∈ X ∧ ∀a : set, a ∈ A → order_rel X a upper ∨ a = upper) → ∃lub : set, lub ∈ X ∧ (∀a : set, a ∈ A → order_rel X a lub ∨ a = lub) ∧ (∀bound : set, bound ∈ X → (∀a : set, a ∈ A → order_rel X a bound ∨ a = bound) → order_rel X lub bound ∨ lub = bound)) HT2).
We prove the intermediate claim HT0: T0.
An exact proof term for the current goal is (andEL T0 (∀x y : set, x ∈ X → y ∈ X → order_rel X x y → ∃z : set, z ∈ X ∧ order_rel X x z ∧ order_rel X z y) HT1).
We prove the intermediate claim Hbetween: ∀x y : set, x ∈ X → y ∈ X → order_rel X x y → ∃z : set, z ∈ X ∧ order_rel X x z ∧ order_rel X z y.
An exact proof term for the current goal is (andER T0 (∀x y : set, x ∈ X → y ∈ X → order_rel X x y → ∃z : set, z ∈ X ∧ order_rel X x z ∧ order_rel X z y) HT1).
We prove the intermediate claim HsoEq: simply_ordered_set X ∧ Tx = order_topology X.
An exact proof term for the current goal is (andEL (simply_ordered_set X ∧ Tx = order_topology X) (∃x y : set, x ∈ X ∧ y ∈ X ∧ x ≠ y) HT0).
We prove the intermediate claim Hso: simply_ordered_set X.
An exact proof term for the current goal is (andEL (simply_ordered_set X) (Tx = order_topology X) HsoEq).
We prove the intermediate claim HTxeq: Tx = order_topology X.
An exact proof term for the current goal is (andER (simply_ordered_set X) (Tx = order_topology X) HsoEq).
rewrite the current goal using HTxeq (from left to right).
We will prove normal_space X (order_topology X).
We will prove one_point_sets_closed X (order_topology X) ∧ ∀A B : set, closed_in X (order_topology X) A → closed_in X (order_topology X) B → A ∩ B = Empty → ∃U V : set, U ∈ order_topology X ∧ V ∈ order_topology X ∧ A ⊆ U ∧ B ⊆ V ∧ U ∩ V = Empty.
Apply andI to the current goal.
We will prove one_point_sets_closed X (order_topology X).
Set Tx0 to be the term order_topology X.
We prove the intermediate claim HH: Hausdorff_space X Tx0.
An exact proof term for the current goal is (ex17_10_order_topology_Hausdorff X Hso).
We will prove topology_on X Tx0 ∧ ∀x : set, x ∈ X → closed_in X Tx0 {x}.
Apply andI to the current goal.
An exact proof term for the current goal is (order_topology_is_topology X Hso).
Let x be given.
Assume HxX: x ∈ X.
An exact proof term for the current goal is (Hausdorff_singletons_closed X Tx0 x HH HxX).
Let A and B be given.
Assume HAcl: closed_in X (order_topology X) A.
Assume HBcl: closed_in X (order_topology X) B.
Assume HAB: A ∩ B = Empty.
We will prove ∃U V : set, U ∈ order_topology X ∧ V ∈ order_topology X ∧ A ⊆ U ∧ B ⊆ V ∧ U ∩ V = Empty.
We prove the intermediate claim HTx0: topology_on X (order_topology X).
An exact proof term for the current goal is (order_topology_is_topology X Hso).
Apply (xm (A = Empty)) to the current goal.
Assume HA0: A = Empty.
Set U to be the term Empty.
Set V to be the term X.
We use U to witness the existential quantifier.
We use V to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is (topology_has_empty X (order_topology X) HTx0).
An exact proof term for the current goal is (topology_has_X X (order_topology X) HTx0).
rewrite the current goal using HA0 (from left to right).
An exact proof term for the current goal is (Subq_Empty U).
We prove the intermediate claim HBsubX: B ⊆ X.
An exact proof term for the current goal is (closed_in_subset X (order_topology X) B HBcl).
An exact proof term for the current goal is HBsubX.
An exact proof term for the current goal is (binintersect_Empty_left X).
Assume HAne: A ≠ Empty.
Apply (xm (B = Empty)) to the current goal.
Assume HB0: B = Empty.
Set U to be the term X.
Set V to be the term Empty.
We use U to witness the existential quantifier.
We use V to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is (topology_has_X X (order_topology X) HTx0).
An exact proof term for the current goal is (topology_has_empty X (order_topology X) HTx0).
We prove the intermediate claim HAsubX: A ⊆ X.
An exact proof term for the current goal is (closed_in_subset X (order_topology X) A HAcl).
An exact proof term for the current goal is HAsubX.
rewrite the current goal using HB0 (from left to right).
An exact proof term for the current goal is (Subq_Empty V).
An exact proof term for the current goal is (binintersect_Empty_right X).
Assume HBne: B ≠ Empty.
We prove the intermediate claim HAsubX: A ⊆ X.
An exact proof term for the current goal is (closed_in_subset X (order_topology X) A HAcl).
We prove the intermediate claim HBsubX: B ⊆ X.
An exact proof term for the current goal is (closed_in_subset X (order_topology X) B HBcl).
We prove the intermediate claim HlinOrd: linear_continuum X (order_topology X).
rewrite the current goal using HTxeq (from right to left).
An exact proof term for the current goal is Hlin.
Set S to be the term X ∖ (A ∪ B).
Set Ts to be the term subspace_topology X (order_topology X) S.
Set pick to be the term λW : set ⇒ Eps_i (λx : set ⇒ x ∈ W).
Set WF to be the term {W0 ∈ 𝒫 S|ex32_8_WFpred X A B S Ts W0}.
Set C to be the term {pick W0|W0 ∈ WF}.
We prove the intermediate claim HSsubX: S ⊆ X.
An exact proof term for the current goal is (setminus_Subq X (A ∪ B)).
We prove the intermediate claim HTs: topology_on S Ts.
An exact proof term for the current goal is (subspace_topology_is_topology X (order_topology X) S HTx0 HSsubX).
We prove the intermediate claim Hchoice: ∀W : set, (∃x : set, x ∈ S ∧ W = component_of S Ts x) → (∃a b : set, a ∈ A ∧ b ∈ B ∧ order_rel X a b ∧ W = order_interval X a b) → ∃cW : set, cW ∈ C ∧ cW ∈ W.
Let W be given.
Assume HcompW: ∃x : set, x ∈ S ∧ W = component_of S Ts x.
Assume HendW: ∃a b : set, a ∈ A ∧ b ∈ B ∧ order_rel X a b ∧ W = order_interval X a b.
Set cW to be the term pick W.
We use cW to witness the existential quantifier.
Apply andI to the current goal.
We will prove cW ∈ C.
We prove the intermediate claim HWsub: W ⊆ S.
Apply HcompW to the current goal.
Let x be given.
Assume Hxpair.
Let y be given.
Assume HyW: y ∈ W.
We prove the intermediate claim HxS: x ∈ S.
An exact proof term for the current goal is (andEL (x ∈ S) (W = component_of S Ts x) Hxpair).
We prove the intermediate claim HWdef: W = component_of S Ts x.
An exact proof term for the current goal is (andER (x ∈ S) (W = component_of S Ts x) Hxpair).
We prove the intermediate claim HyComp: y ∈ component_of S Ts x.
rewrite the current goal using HWdef (from right to left).
An exact proof term for the current goal is HyW.
An exact proof term for the current goal is (SepE1 S (λy0 : set ⇒ ∃C0 : set, connected_space C0 (subspace_topology S Ts C0) ∧ x ∈ C0 ∧ y0 ∈ C0) y HyComp).
We prove the intermediate claim HWpow: W ∈ 𝒫 S.
An exact proof term for the current goal is (PowerI S W HWsub).
We prove the intermediate claim HWWF: W ∈ WF.
Apply SepI to the current goal.
An exact proof term for the current goal is HWpow.
We prove the intermediate claim HWFpredW: ex32_8_WFpred X A B S Ts W = ((∃x : set, x ∈ S ∧ W = component_of S Ts x) ∧ (∃a b : set, a ∈ A ∧ b ∈ B ∧ order_rel X a b ∧ W = order_interval X a b)).
Use reflexivity.
rewrite the current goal using HWFpredW (from left to right).
Apply andI to the current goal.
An exact proof term for the current goal is HcompW.
An exact proof term for the current goal is HendW.
An exact proof term for the current goal is (ReplI WF (λW0 : set ⇒ pick W0) W HWWF).
We prove the intermediate claim HexxW: ∃x : set, x ∈ W.
Apply HcompW to the current goal.
Let x be given.
Assume Hxpair.
We prove the intermediate claim HxS: x ∈ S.
An exact proof term for the current goal is (andEL (x ∈ S) (W = component_of S Ts x) Hxpair).
We prove the intermediate claim HWdef: W = component_of S Ts x.
An exact proof term for the current goal is (andER (x ∈ S) (W = component_of S Ts x) Hxpair).
We prove the intermediate claim HxComp: x ∈ component_of S Ts x.
An exact proof term for the current goal is (point_in_component S Ts x HTs HxS).
We use x to witness the existential quantifier.
rewrite the current goal using HWdef (from left to right).
An exact proof term for the current goal is HxComp.
An exact proof term for the current goal is (Eps_i_ex (λx : set ⇒ x ∈ W) HexxW).
We prove the intermediate claim HCsubX0: C ⊆ X.
Let c be given.
Assume HcC: c ∈ C.
We prove the intermediate claim HexW0: ∃W0 ∈ WF, c = pick W0.
An exact proof term for the current goal is (ReplE WF (λW0 : set ⇒ pick W0) c HcC).
Apply HexW0 to the current goal.
Let W0 be given.
Assume HW0pair.
We prove the intermediate claim HW0WF: W0 ∈ WF.
An exact proof term for the current goal is (andEL (W0 ∈ WF) (c = pick W0) HW0pair).
We prove the intermediate claim HcEq: c = pick W0.
An exact proof term for the current goal is (andER (W0 ∈ WF) (c = pick W0) HW0pair).
rewrite the current goal using HcEq (from left to right).
We prove the intermediate claim HW0Pow: W0 ∈ 𝒫 S.
An exact proof term for the current goal is (SepE1 (𝒫 S) (λW1 : set ⇒ ex32_8_WFpred X A B S Ts W1) W0 HW0WF).
We prove the intermediate claim HW0subS: W0 ⊆ S.
An exact proof term for the current goal is (PowerE S W0 HW0Pow).
We prove the intermediate claim HWFpred: ex32_8_WFpred X A B S Ts W0.
An exact proof term for the current goal is (SepE2 (𝒫 S) (λW1 : set ⇒ ex32_8_WFpred X A B S Ts W1) W0 HW0WF).
We prove the intermediate claim Hexx0: ∃x0 : set, x0 ∈ S ∧ W0 = component_of S Ts x0.
An exact proof term for the current goal is (andEL (∃x0 : set, x0 ∈ S ∧ W0 = component_of S Ts x0) (∃a0 b0 : set, a0 ∈ A ∧ b0 ∈ B ∧ order_rel X a0 b0 ∧ W0 = order_interval X a0 b0) HWFpred).
We prove the intermediate claim HexxW0: ∃x0 : set, x0 ∈ W0.
Apply Hexx0 to the current goal.
Let x0 be given.
Assume Hx0pair.
We prove the intermediate claim Hx0S: x0 ∈ S.
An exact proof term for the current goal is (andEL (x0 ∈ S) (W0 = component_of S Ts x0) Hx0pair).
We prove the intermediate claim HW0Eq: W0 = component_of S Ts x0.
An exact proof term for the current goal is (andER (x0 ∈ S) (W0 = component_of S Ts x0) Hx0pair).
We prove the intermediate claim Hx0W0: x0 ∈ W0.
rewrite the current goal using HW0Eq (from left to right).
An exact proof term for the current goal is (point_in_component S Ts x0 HTs Hx0S).
We use x0 to witness the existential quantifier.
An exact proof term for the current goal is Hx0W0.
We prove the intermediate claim HpickW0: pick W0 ∈ W0.
An exact proof term for the current goal is (Eps_i_ex (λx0 : set ⇒ x0 ∈ W0) HexxW0).
We prove the intermediate claim HpickS: pick W0 ∈ S.
An exact proof term for the current goal is (HW0subS (pick W0) HpickW0).
An exact proof term for the current goal is (HSsubX (pick W0) HpickS).
We prove the intermediate claim HCcl: closed_in X (order_topology X) C.
We prove the intermediate claim HSdef: S = X ∖ (A ∪ B).
Use reflexivity.
We prove the intermediate claim HTsdef: Ts = subspace_topology X (order_topology X) S.
Use reflexivity.
We prove the intermediate claim HWFdef: WF = {W0 ∈ 𝒫 S|ex32_8_WFpred X A B S Ts W0}.
Use reflexivity.
We prove the intermediate claim HCdef: C = {pick W0|W0 ∈ WF}.
Use reflexivity.
We prove the intermediate claim HpickAll: ∀W : set, W ∈ WF → pick W ∈ W.
Let W be given.
Assume HW: W ∈ WF.
We prove the intermediate claim HWpred: ex32_8_WFpred X A B S Ts W.
We prove the intermediate claim HW': W ∈ {W1 ∈ 𝒫 S|ex32_8_WFpred X A B S Ts W1}.
rewrite the current goal using HWFdef (from right to left).
An exact proof term for the current goal is HW.
An exact proof term for the current goal is (SepE2 (𝒫 S) (λW1 : set ⇒ ex32_8_WFpred X A B S Ts W1) W HW').
We prove the intermediate claim Hexx: ∃x0 : set, x0 ∈ S ∧ W = component_of S Ts x0.
An exact proof term for the current goal is (andEL (∃x0 : set, x0 ∈ S ∧ W = component_of S Ts x0) (∃a0 b0 : set, a0 ∈ A ∧ b0 ∈ B ∧ order_rel X a0 b0 ∧ W = order_interval X a0 b0) HWpred).
We prove the intermediate claim HexxW: ∃x0 : set, x0 ∈ W.
Apply Hexx to the current goal.
Let x0 be given.
Assume Hx0pair.
We prove the intermediate claim Hx0S: x0 ∈ S.
An exact proof term for the current goal is (andEL (x0 ∈ S) (W = component_of S Ts x0) Hx0pair).
We prove the intermediate claim HWdef: W = component_of S Ts x0.
An exact proof term for the current goal is (andER (x0 ∈ S) (W = component_of S Ts x0) Hx0pair).
We prove the intermediate claim Hx0W: x0 ∈ W.
rewrite the current goal using HWdef (from left to right).
An exact proof term for the current goal is (point_in_component S Ts x0 HTs Hx0S).
We use x0 to witness the existential quantifier.
An exact proof term for the current goal is Hx0W.
An exact proof term for the current goal is (Eps_i_ex (λx0 : set ⇒ x0 ∈ W) HexxW).
An exact proof term for the current goal is (ex32_8b_chosen_points_set_closed X (order_topology X) A B S Ts WF C pick HlinOrd HAcl HBcl HAB HSdef HTsdef HWFdef HCdef HpickAll).
We prove the intermediate claim HCne: C ≠ Empty.
Apply (xm (C = Empty)) to the current goal.
Assume HC0: C = Empty.
We will prove False.
We prove the intermediate claim Hexa0: ∃a0 : set, a0 ∈ A.
An exact proof term for the current goal is (nonempty_has_element A HAne).
Apply Hexa0 to the current goal.
Let a0 be given.
Assume Ha0A: a0 ∈ A.
We prove the intermediate claim Hexb0: ∃b0 : set, b0 ∈ B.
An exact proof term for the current goal is (nonempty_has_element B HBne).
Apply Hexb0 to the current goal.
Let b0 be given.
Assume Hb0B: b0 ∈ B.
We prove the intermediate claim Ha0X: a0 ∈ X.
An exact proof term for the current goal is (HAsubX a0 Ha0A).
We prove the intermediate claim Hb0X: b0 ∈ X.
An exact proof term for the current goal is (HBsubX b0 Hb0B).
We prove the intermediate claim Ha0in: a0 ∈ (X ∖ C).
rewrite the current goal using HC0 (from left to right).
rewrite the current goal using (setminus_Empty_eq X) (from left to right).
An exact proof term for the current goal is Ha0X.
We prove the intermediate claim HconnX0: connected_space X (order_topology X).
An exact proof term for the current goal is (thm24_1_linear_continuum_connected X (order_topology X) HlinOrd).
We prove the intermediate claim Hsubeq: subspace_topology X (order_topology X) X = order_topology X.
An exact proof term for the current goal is (subspace_topology_whole X (order_topology X) HTx0).
We prove the intermediate claim Hcompa0: component_of (X ∖ C) (subspace_topology X (order_topology X) (X ∖ C)) a0 = X.
rewrite the current goal using HC0 (from left to right).
rewrite the current goal using (setminus_Empty_eq X) (from left to right).
rewrite the current goal using Hsubeq (from left to right).
An exact proof term for the current goal is (component_of_whole X (order_topology X) a0 HconnX0 Ha0X).
We prove the intermediate claim Ha0Comp: a0 ∈ component_of (X ∖ C) (subspace_topology X (order_topology X) (X ∖ C)) a0.
rewrite the current goal using Hcompa0 (from left to right).
An exact proof term for the current goal is Ha0X.
We prove the intermediate claim Hb0Comp: b0 ∈ component_of (X ∖ C) (subspace_topology X (order_topology X) (X ∖ C)) a0.
rewrite the current goal using Hcompa0 (from left to right).
An exact proof term for the current goal is Hb0X.
We prove the intermediate claim HnoBoth: ¬ (∃a b : set, a ∈ A ∧ b ∈ B ∧ a ∈ component_of (X ∖ C) (subspace_topology X (order_topology X) (X ∖ C)) a0 ∧ b ∈ component_of (X ∖ C) (subspace_topology X (order_topology X) (X ∖ C)) a0).
An exact proof term for the current goal is (ex32_8c_component_of_X_minus_C_not_both X (order_topology X) A B C HlinOrd HAcl HBcl HAB Hchoice HCcl a0 Ha0in).
We prove the intermediate claim HexBoth: ∃a b : set, a ∈ A ∧ b ∈ B ∧ a ∈ component_of (X ∖ C) (subspace_topology X (order_topology X) (X ∖ C)) a0 ∧ b ∈ component_of (X ∖ C) (subspace_topology X (order_topology X) (X ∖ C)) a0.
We use a0 to witness the existential quantifier.
We use b0 to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Ha0A.
An exact proof term for the current goal is Hb0B.
An exact proof term for the current goal is Ha0Comp.
An exact proof term for the current goal is Hb0Comp.
An exact proof term for the current goal is (HnoBoth HexBoth).
Assume HCne0: C ≠ Empty.
An exact proof term for the current goal is HCne0.
Set Y to be the term X ∖ C.
Set Ty to be the term subspace_topology X (order_topology X) Y.
Set UFamA to be the term {component_of Y Ty a|a ∈ A}.
Set UFamB to be the term {component_of Y Ty b|b ∈ B}.
Set U to be the term ⋃ UFamA.
Set V to be the term ⋃ UFamB.
We prove the intermediate claim HCsubS0: C ⊆ S.
Let c be given.
Assume HcC: c ∈ C.
We prove the intermediate claim HexW: ∃W0 ∈ WF, c = pick W0.
An exact proof term for the current goal is (ReplE WF (λW0 : set ⇒ pick W0) c HcC).
Apply HexW to the current goal.
Let W0 be given.
Assume HW0pair.
We prove the intermediate claim HW0WF: W0 ∈ WF.
An exact proof term for the current goal is (andEL (W0 ∈ WF) (c = pick W0) HW0pair).
We prove the intermediate claim Hcdef: c = pick W0.
An exact proof term for the current goal is (andER (W0 ∈ WF) (c = pick W0) HW0pair).
We prove the intermediate claim HW0pow: W0 ∈ 𝒫 S.
An exact proof term for the current goal is (SepE1 (𝒫 S) (λW1 : set ⇒ ex32_8_WFpred X A B S Ts W1) W0 HW0WF).
We prove the intermediate claim HW0subS: W0 ⊆ S.
An exact proof term for the current goal is (PowerE S W0 HW0pow).
We prove the intermediate claim HWFpredW0: ex32_8_WFpred X A B S Ts W0 = ((∃x : set, x ∈ S ∧ W0 = component_of S Ts x) ∧ (∃a b : set, a ∈ A ∧ b ∈ B ∧ order_rel X a b ∧ W0 = order_interval X a b)).
Use reflexivity.
We prove the intermediate claim HpairW0: (∃x : set, x ∈ S ∧ W0 = component_of S Ts x) ∧ (∃a b : set, a ∈ A ∧ b ∈ B ∧ order_rel X a b ∧ W0 = order_interval X a b).
rewrite the current goal using HWFpredW0 (from right to left).
An exact proof term for the current goal is (SepE2 (𝒫 S) (λW1 : set ⇒ ex32_8_WFpred X A B S Ts W1) W0 HW0WF).
We prove the intermediate claim HcompW0: ∃x : set, x ∈ S ∧ W0 = component_of S Ts x.
An exact proof term for the current goal is (andEL (∃x : set, x ∈ S ∧ W0 = component_of S Ts x) (∃a b : set, a ∈ A ∧ b ∈ B ∧ order_rel X a b ∧ W0 = order_interval X a b) HpairW0).
We prove the intermediate claim HpickW0: pick W0 ∈ W0.
Apply HcompW0 to the current goal.
Let x be given.
Assume Hxpair.
We prove the intermediate claim HxS: x ∈ S.
An exact proof term for the current goal is (andEL (x ∈ S) (W0 = component_of S Ts x) Hxpair).
We prove the intermediate claim HW0def: W0 = component_of S Ts x.
An exact proof term for the current goal is (andER (x ∈ S) (W0 = component_of S Ts x) Hxpair).
We prove the intermediate claim HxComp: x ∈ component_of S Ts x.
An exact proof term for the current goal is (point_in_component S Ts x HTs HxS).
We prove the intermediate claim HxW0: x ∈ W0.
rewrite the current goal using HW0def (from left to right).
An exact proof term for the current goal is HxComp.
We prove the intermediate claim Hexx: ∃y : set, y ∈ W0.
We use x to witness the existential quantifier.
An exact proof term for the current goal is HxW0.
An exact proof term for the current goal is (Eps_i_ex (λy : set ⇒ y ∈ W0) Hexx).
We prove the intermediate claim HpickS: pick W0 ∈ S.
An exact proof term for the current goal is (HW0subS (pick W0) HpickW0).
rewrite the current goal using Hcdef (from left to right).
An exact proof term for the current goal is HpickS.
We prove the intermediate claim HcompOpen: ∀x : set, x ∈ Y → component_of Y Ty x ∈ order_topology X.
Let x be given.
Assume HxY: x ∈ Y.
We prove the intermediate claim HlocX: locally_connected X (order_topology X).
An exact proof term for the current goal is (linear_continuum_locally_connected X (order_topology X) HlinOrd).
We prove the intermediate claim HYopen_in: open_in X (order_topology X) Y.
An exact proof term for the current goal is (open_of_closed_complement X (order_topology X) C HCcl).
We prove the intermediate claim HYopen: Y ∈ order_topology X.
An exact proof term for the current goal is (open_in_elem X (order_topology X) Y HYopen_in).
We prove the intermediate claim HlocY: locally_connected Y Ty.
An exact proof term for the current goal is (open_subspace_locally_connected X (order_topology X) Y HlocX HYopen).
We prove the intermediate claim HcompOpenY: open_in Y Ty (component_of Y Ty x).
An exact proof term for the current goal is (components_are_open_in_locally_connected Y Ty HlocY x HxY).
We prove the intermediate claim HcompTy: component_of Y Ty x ∈ Ty.
An exact proof term for the current goal is (open_in_elem Y Ty (component_of Y Ty x) HcompOpenY).
We prove the intermediate claim HexV0: ∃V0 ∈ order_topology X, component_of Y Ty x = V0 ∩ Y.
An exact proof term for the current goal is (subspace_topologyE X (order_topology X) Y (component_of Y Ty x) HcompTy).
Apply HexV0 to the current goal.
Let V0 be given.
Assume HV0pair.
We prove the intermediate claim HV0open: V0 ∈ order_topology X.
An exact proof term for the current goal is (andEL (V0 ∈ order_topology X) (component_of Y Ty x = V0 ∩ Y) HV0pair).
We prove the intermediate claim Heq: component_of Y Ty x = V0 ∩ Y.
An exact proof term for the current goal is (andER (V0 ∈ order_topology X) (component_of Y Ty x = V0 ∩ Y) HV0pair).
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is (topology_binintersect_closed X (order_topology X) V0 Y HTx0 HV0open HYopen).
We use U to witness the existential quantifier.
We use V to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
We will prove U ∈ order_topology X.
We prove the intermediate claim HUFamAsub: UFamA ⊆ order_topology X.
Let D be given.
Assume HD: D ∈ UFamA.
We prove the intermediate claim Hexa: ∃a : set, a ∈ A ∧ D = component_of Y Ty a.
An exact proof term for the current goal is (ReplE A (λa0 : set ⇒ component_of Y Ty a0) D HD).
Apply Hexa to the current goal.
Let a be given.
Assume Hapair.
We prove the intermediate claim HaA: a ∈ A.
An exact proof term for the current goal is (andEL (a ∈ A) (D = component_of Y Ty a) Hapair).
We prove the intermediate claim HDeq: D = component_of Y Ty a.
An exact proof term for the current goal is (andER (a ∈ A) (D = component_of Y Ty a) Hapair).
We prove the intermediate claim HaX: a ∈ X.
An exact proof term for the current goal is (HAsubX a HaA).
We prove the intermediate claim HaNotC: a ∉ C.
Assume HaC: a ∈ C.
We prove the intermediate claim HaS: a ∈ S.
An exact proof term for the current goal is (HCsubS0 a HaC).
We prove the intermediate claim HaNotAB: a ∉ (A ∪ B).
An exact proof term for the current goal is (setminusE2 X (A ∪ B) a HaS).
We prove the intermediate claim HaAB: a ∈ (A ∪ B).
An exact proof term for the current goal is (binunionI1 A B a HaA).
An exact proof term for the current goal is (HaNotAB HaAB).
We prove the intermediate claim HaY: a ∈ Y.
Apply setminusI to the current goal.
An exact proof term for the current goal is HaX.
An exact proof term for the current goal is HaNotC.
rewrite the current goal using HDeq (from left to right).
An exact proof term for the current goal is (HcompOpen a HaY).
An exact proof term for the current goal is (topology_union_closed X (order_topology X) UFamA HTx0 HUFamAsub).
We will prove V ∈ order_topology X.
We prove the intermediate claim HUFamBsub: UFamB ⊆ order_topology X.
Let D be given.
Assume HD: D ∈ UFamB.
We prove the intermediate claim Hexb: ∃b : set, b ∈ B ∧ D = component_of Y Ty b.
An exact proof term for the current goal is (ReplE B (λb0 : set ⇒ component_of Y Ty b0) D HD).
Apply Hexb to the current goal.
Let b be given.
Assume Hbpair.
We prove the intermediate claim HbB: b ∈ B.
An exact proof term for the current goal is (andEL (b ∈ B) (D = component_of Y Ty b) Hbpair).
We prove the intermediate claim HDeq: D = component_of Y Ty b.
An exact proof term for the current goal is (andER (b ∈ B) (D = component_of Y Ty b) Hbpair).
We prove the intermediate claim HbX: b ∈ X.
An exact proof term for the current goal is (HBsubX b HbB).
We prove the intermediate claim HbNotC: b ∉ C.
Assume HbC: b ∈ C.
We prove the intermediate claim HbS: b ∈ S.
An exact proof term for the current goal is (HCsubS0 b HbC).
We prove the intermediate claim HbNotAB: b ∉ (A ∪ B).
An exact proof term for the current goal is (setminusE2 X (A ∪ B) b HbS).
We prove the intermediate claim HbAB: b ∈ (A ∪ B).
An exact proof term for the current goal is (binunionI2 A B b HbB).
An exact proof term for the current goal is (HbNotAB HbAB).
We prove the intermediate claim HbY: b ∈ Y.
Apply setminusI to the current goal.
An exact proof term for the current goal is HbX.
An exact proof term for the current goal is HbNotC.
rewrite the current goal using HDeq (from left to right).
An exact proof term for the current goal is (HcompOpen b HbY).
An exact proof term for the current goal is (topology_union_closed X (order_topology X) UFamB HTx0 HUFamBsub).
We will prove A ⊆ U.
Let a be given.
Assume HaA: a ∈ A.
We will prove a ∈ U.
We prove the intermediate claim HaX: a ∈ X.
An exact proof term for the current goal is (HAsubX a HaA).
We prove the intermediate claim HCsubS: C ⊆ S.
Let c be given.
Assume HcC: c ∈ C.
We prove the intermediate claim HexW: ∃W0 ∈ WF, c = pick W0.
An exact proof term for the current goal is (ReplE WF (λW0 : set ⇒ pick W0) c HcC).
Apply HexW to the current goal.
Let W0 be given.
Assume HW0pair.
We prove the intermediate claim HW0WF: W0 ∈ WF.
An exact proof term for the current goal is (andEL (W0 ∈ WF) (c = pick W0) HW0pair).
We prove the intermediate claim Hcdef: c = pick W0.
An exact proof term for the current goal is (andER (W0 ∈ WF) (c = pick W0) HW0pair).
We prove the intermediate claim HW0pow: W0 ∈ 𝒫 S.
An exact proof term for the current goal is (SepE1 (𝒫 S) (λW1 : set ⇒ ex32_8_WFpred X A B S Ts W1) W0 HW0WF).
We prove the intermediate claim HW0subS: W0 ⊆ S.
An exact proof term for the current goal is (PowerE S W0 HW0pow).
We prove the intermediate claim HWFpredW0: ex32_8_WFpred X A B S Ts W0 = ((∃x : set, x ∈ S ∧ W0 = component_of S Ts x) ∧ (∃a b : set, a ∈ A ∧ b ∈ B ∧ order_rel X a b ∧ W0 = order_interval X a b)).
Use reflexivity.
We prove the intermediate claim HpairW0: (∃x : set, x ∈ S ∧ W0 = component_of S Ts x) ∧ (∃a b : set, a ∈ A ∧ b ∈ B ∧ order_rel X a b ∧ W0 = order_interval X a b).
rewrite the current goal using HWFpredW0 (from right to left).
An exact proof term for the current goal is (SepE2 (𝒫 S) (λW1 : set ⇒ ex32_8_WFpred X A B S Ts W1) W0 HW0WF).
We prove the intermediate claim HcompW0: ∃x : set, x ∈ S ∧ W0 = component_of S Ts x.
An exact proof term for the current goal is (andEL (∃x : set, x ∈ S ∧ W0 = component_of S Ts x) (∃a b : set, a ∈ A ∧ b ∈ B ∧ order_rel X a b ∧ W0 = order_interval X a b) HpairW0).
We prove the intermediate claim HpickW0: pick W0 ∈ W0.
Apply HcompW0 to the current goal.
Let x be given.
Assume Hxpair.
We prove the intermediate claim HxS: x ∈ S.
An exact proof term for the current goal is (andEL (x ∈ S) (W0 = component_of S Ts x) Hxpair).
We prove the intermediate claim HW0def: W0 = component_of S Ts x.
An exact proof term for the current goal is (andER (x ∈ S) (W0 = component_of S Ts x) Hxpair).
We prove the intermediate claim HxComp: x ∈ component_of S Ts x.
An exact proof term for the current goal is (point_in_component S Ts x HTs HxS).
We prove the intermediate claim HxW0: x ∈ W0.
rewrite the current goal using HW0def (from left to right).
An exact proof term for the current goal is HxComp.
We prove the intermediate claim Hexx: ∃y : set, y ∈ W0.
We use x to witness the existential quantifier.
An exact proof term for the current goal is HxW0.
An exact proof term for the current goal is (Eps_i_ex (λy : set ⇒ y ∈ W0) Hexx).
We prove the intermediate claim HpickS: pick W0 ∈ S.
An exact proof term for the current goal is (HW0subS (pick W0) HpickW0).
rewrite the current goal using Hcdef (from left to right).
An exact proof term for the current goal is HpickS.
We prove the intermediate claim HaNotC: a ∉ C.
Assume HaC: a ∈ C.
We prove the intermediate claim HaS: a ∈ S.
An exact proof term for the current goal is (HCsubS a HaC).
We prove the intermediate claim HaNotAB: a ∉ (A ∪ B).
An exact proof term for the current goal is (setminusE2 X (A ∪ B) a HaS).
We prove the intermediate claim HaAB: a ∈ (A ∪ B).
An exact proof term for the current goal is (binunionI1 A B a HaA).
An exact proof term for the current goal is (HaNotAB HaAB).
We prove the intermediate claim HaY: a ∈ Y.
Apply setminusI to the current goal.
An exact proof term for the current goal is HaX.
An exact proof term for the current goal is HaNotC.
We prove the intermediate claim HTy: topology_on Y Ty.
An exact proof term for the current goal is (subspace_topology_is_topology X (order_topology X) Y HTx0 (setminus_Subq X C)).
We prove the intermediate claim HaComp: a ∈ component_of Y Ty a.
An exact proof term for the current goal is (point_in_component Y Ty a HTy HaY).
We prove the intermediate claim HaFam: component_of Y Ty a ∈ UFamA.
An exact proof term for the current goal is (ReplI A (λa0 : set ⇒ component_of Y Ty a0) a HaA).
An exact proof term for the current goal is (UnionI UFamA a (component_of Y Ty a) HaComp HaFam).
We will prove B ⊆ V.
Let b be given.
Assume HbB: b ∈ B.
We will prove b ∈ V.
We prove the intermediate claim HbX: b ∈ X.
An exact proof term for the current goal is (HBsubX b HbB).
We prove the intermediate claim HCsubS: C ⊆ S.
Let c be given.
Assume HcC: c ∈ C.
We prove the intermediate claim HexW: ∃W0 ∈ WF, c = pick W0.
An exact proof term for the current goal is (ReplE WF (λW0 : set ⇒ pick W0) c HcC).
Apply HexW to the current goal.
Let W0 be given.
Assume HW0pair.
We prove the intermediate claim HW0WF: W0 ∈ WF.
An exact proof term for the current goal is (andEL (W0 ∈ WF) (c = pick W0) HW0pair).
We prove the intermediate claim Hcdef: c = pick W0.
An exact proof term for the current goal is (andER (W0 ∈ WF) (c = pick W0) HW0pair).
We prove the intermediate claim HW0pow: W0 ∈ 𝒫 S.
An exact proof term for the current goal is (SepE1 (𝒫 S) (λW1 : set ⇒ ex32_8_WFpred X A B S Ts W1) W0 HW0WF).
We prove the intermediate claim HW0subS: W0 ⊆ S.
An exact proof term for the current goal is (PowerE S W0 HW0pow).
We prove the intermediate claim HWFpredW0: ex32_8_WFpred X A B S Ts W0 = ((∃x : set, x ∈ S ∧ W0 = component_of S Ts x) ∧ (∃a b : set, a ∈ A ∧ b ∈ B ∧ order_rel X a b ∧ W0 = order_interval X a b)).
Use reflexivity.
We prove the intermediate claim HpairW0: (∃x : set, x ∈ S ∧ W0 = component_of S Ts x) ∧ (∃a b : set, a ∈ A ∧ b ∈ B ∧ order_rel X a b ∧ W0 = order_interval X a b).
rewrite the current goal using HWFpredW0 (from right to left).
An exact proof term for the current goal is (SepE2 (𝒫 S) (λW1 : set ⇒ ex32_8_WFpred X A B S Ts W1) W0 HW0WF).
We prove the intermediate claim HcompW0: ∃x : set, x ∈ S ∧ W0 = component_of S Ts x.
An exact proof term for the current goal is (andEL (∃x : set, x ∈ S ∧ W0 = component_of S Ts x) (∃a b : set, a ∈ A ∧ b ∈ B ∧ order_rel X a b ∧ W0 = order_interval X a b) HpairW0).
We prove the intermediate claim HpickW0: pick W0 ∈ W0.
Apply HcompW0 to the current goal.
Let x be given.
Assume Hxpair.
We prove the intermediate claim HxS: x ∈ S.
An exact proof term for the current goal is (andEL (x ∈ S) (W0 = component_of S Ts x) Hxpair).
We prove the intermediate claim HW0def: W0 = component_of S Ts x.
An exact proof term for the current goal is (andER (x ∈ S) (W0 = component_of S Ts x) Hxpair).
We prove the intermediate claim HxComp: x ∈ component_of S Ts x.
An exact proof term for the current goal is (point_in_component S Ts x HTs HxS).
We prove the intermediate claim HxW0: x ∈ W0.
rewrite the current goal using HW0def (from left to right).
An exact proof term for the current goal is HxComp.
We prove the intermediate claim Hexx: ∃y : set, y ∈ W0.
We use x to witness the existential quantifier.
An exact proof term for the current goal is HxW0.
An exact proof term for the current goal is (Eps_i_ex (λy : set ⇒ y ∈ W0) Hexx).
We prove the intermediate claim HpickS: pick W0 ∈ S.
An exact proof term for the current goal is (HW0subS (pick W0) HpickW0).
rewrite the current goal using Hcdef (from left to right).
An exact proof term for the current goal is HpickS.
We prove the intermediate claim HbNotC: b ∉ C.
Assume HbC: b ∈ C.
We prove the intermediate claim HbS: b ∈ S.
An exact proof term for the current goal is (HCsubS b HbC).
We prove the intermediate claim HbNotAB: b ∉ (A ∪ B).
An exact proof term for the current goal is (setminusE2 X (A ∪ B) b HbS).
We prove the intermediate claim HbAB: b ∈ (A ∪ B).
An exact proof term for the current goal is (binunionI2 A B b HbB).
An exact proof term for the current goal is (HbNotAB HbAB).
We prove the intermediate claim HbY: b ∈ Y.
Apply setminusI to the current goal.
An exact proof term for the current goal is HbX.
An exact proof term for the current goal is HbNotC.
We prove the intermediate claim HTy: topology_on Y Ty.
An exact proof term for the current goal is (subspace_topology_is_topology X (order_topology X) Y HTx0 (setminus_Subq X C)).
We prove the intermediate claim HbComp: b ∈ component_of Y Ty b.
An exact proof term for the current goal is (point_in_component Y Ty b HTy HbY).
We prove the intermediate claim HbFam: component_of Y Ty b ∈ UFamB.
An exact proof term for the current goal is (ReplI B (λb0 : set ⇒ component_of Y Ty b0) b HbB).
An exact proof term for the current goal is (UnionI UFamB b (component_of Y Ty b) HbComp HbFam).
Apply set_ext to the current goal.
Let x be given.
Assume HxUV: x ∈ U ∩ V.
We will prove x ∈ Empty.
We prove the intermediate claim HxU: x ∈ U.
An exact proof term for the current goal is (binintersectE1 U V x HxUV).
We prove the intermediate claim HxV: x ∈ V.
An exact proof term for the current goal is (binintersectE2 U V x HxUV).
We prove the intermediate claim HexDU: ∃D : set, x ∈ D ∧ D ∈ UFamA.
An exact proof term for the current goal is (UnionE UFamA x HxU).
We prove the intermediate claim HexDV: ∃E : set, x ∈ E ∧ E ∈ UFamB.
An exact proof term for the current goal is (UnionE UFamB x HxV).
Apply HexDU to the current goal.
Let D be given.
Assume HDpair.
We prove the intermediate claim HxD: x ∈ D.
An exact proof term for the current goal is (andEL (x ∈ D) (D ∈ UFamA) HDpair).
We prove the intermediate claim HDin: D ∈ UFamA.
An exact proof term for the current goal is (andER (x ∈ D) (D ∈ UFamA) HDpair).
Apply HexDV to the current goal.
Let E be given.
Assume HEpair.
We prove the intermediate claim HxE: x ∈ E.
An exact proof term for the current goal is (andEL (x ∈ E) (E ∈ UFamB) HEpair).
We prove the intermediate claim HEin: E ∈ UFamB.
An exact proof term for the current goal is (andER (x ∈ E) (E ∈ UFamB) HEpair).
We prove the intermediate claim Hexa: ∃a : set, a ∈ A ∧ D = component_of Y Ty a.
An exact proof term for the current goal is (ReplE A (λa0 : set ⇒ component_of Y Ty a0) D HDin).
We prove the intermediate claim Hexb: ∃b : set, b ∈ B ∧ E = component_of Y Ty b.
An exact proof term for the current goal is (ReplE B (λb0 : set ⇒ component_of Y Ty b0) E HEin).
Apply Hexa to the current goal.
Let a be given.
Assume Hapair.
We prove the intermediate claim HaA: a ∈ A.
An exact proof term for the current goal is (andEL (a ∈ A) (D = component_of Y Ty a) Hapair).
We prove the intermediate claim HDeq: D = component_of Y Ty a.
An exact proof term for the current goal is (andER (a ∈ A) (D = component_of Y Ty a) Hapair).
Apply Hexb to the current goal.
Let b be given.
Assume Hbpair.
We prove the intermediate claim HbB: b ∈ B.
An exact proof term for the current goal is (andEL (b ∈ B) (E = component_of Y Ty b) Hbpair).
We prove the intermediate claim HEeq: E = component_of Y Ty b.
An exact proof term for the current goal is (andER (b ∈ B) (E = component_of Y Ty b) Hbpair).
We prove the intermediate claim HTy: topology_on Y Ty.
An exact proof term for the current goal is (subspace_topology_is_topology X (order_topology X) Y HTx0 (setminus_Subq X C)).
We prove the intermediate claim HaX: a ∈ X.
An exact proof term for the current goal is (HAsubX a HaA).
We prove the intermediate claim HbX: b ∈ X.
An exact proof term for the current goal is (HBsubX b HbB).
We prove the intermediate claim HCsubS: C ⊆ S.
Let c be given.
Assume HcC: c ∈ C.
We prove the intermediate claim HexW: ∃W0 ∈ WF, c = pick W0.
An exact proof term for the current goal is (ReplE WF (λW0 : set ⇒ pick W0) c HcC).
Apply HexW to the current goal.
Let W0 be given.
Assume HW0pair.
We prove the intermediate claim HW0WF: W0 ∈ WF.
An exact proof term for the current goal is (andEL (W0 ∈ WF) (c = pick W0) HW0pair).
We prove the intermediate claim Hcdef: c = pick W0.
An exact proof term for the current goal is (andER (W0 ∈ WF) (c = pick W0) HW0pair).
We prove the intermediate claim HW0pow: W0 ∈ 𝒫 S.
An exact proof term for the current goal is (SepE1 (𝒫 S) (λW1 : set ⇒ ex32_8_WFpred X A B S Ts W1) W0 HW0WF).
We prove the intermediate claim HW0subS: W0 ⊆ S.
An exact proof term for the current goal is (PowerE S W0 HW0pow).
We prove the intermediate claim HWFpredW0: ex32_8_WFpred X A B S Ts W0 = ((∃x0 : set, x0 ∈ S ∧ W0 = component_of S Ts x0) ∧ (∃a0 b0 : set, a0 ∈ A ∧ b0 ∈ B ∧ order_rel X a0 b0 ∧ W0 = order_interval X a0 b0)).
Use reflexivity.
We prove the intermediate claim HpairW0: (∃x0 : set, x0 ∈ S ∧ W0 = component_of S Ts x0) ∧ (∃a0 b0 : set, a0 ∈ A ∧ b0 ∈ B ∧ order_rel X a0 b0 ∧ W0 = order_interval X a0 b0).
rewrite the current goal using HWFpredW0 (from right to left).
An exact proof term for the current goal is (SepE2 (𝒫 S) (λW1 : set ⇒ ex32_8_WFpred X A B S Ts W1) W0 HW0WF).
We prove the intermediate claim HcompW0: ∃x0 : set, x0 ∈ S ∧ W0 = component_of S Ts x0.
An exact proof term for the current goal is (andEL (∃x0 : set, x0 ∈ S ∧ W0 = component_of S Ts x0) (∃a0 b0 : set, a0 ∈ A ∧ b0 ∈ B ∧ order_rel X a0 b0 ∧ W0 = order_interval X a0 b0) HpairW0).
We prove the intermediate claim HpickW0: pick W0 ∈ W0.
Apply HcompW0 to the current goal.
Let x0 be given.
Assume Hx0pair.
We prove the intermediate claim Hx0S: x0 ∈ S.
An exact proof term for the current goal is (andEL (x0 ∈ S) (W0 = component_of S Ts x0) Hx0pair).
We prove the intermediate claim HW0def: W0 = component_of S Ts x0.
An exact proof term for the current goal is (andER (x0 ∈ S) (W0 = component_of S Ts x0) Hx0pair).
We prove the intermediate claim Hx0Comp: x0 ∈ component_of S Ts x0.
An exact proof term for the current goal is (point_in_component S Ts x0 HTs Hx0S).
We prove the intermediate claim Hx0W0: x0 ∈ W0.
rewrite the current goal using HW0def (from left to right).
An exact proof term for the current goal is Hx0Comp.
We prove the intermediate claim Hexx0: ∃y0 : set, y0 ∈ W0.
We use x0 to witness the existential quantifier.
An exact proof term for the current goal is Hx0W0.
An exact proof term for the current goal is (Eps_i_ex (λy0 : set ⇒ y0 ∈ W0) Hexx0).
We prove the intermediate claim HpickS: pick W0 ∈ S.
An exact proof term for the current goal is (HW0subS (pick W0) HpickW0).
rewrite the current goal using Hcdef (from left to right).
An exact proof term for the current goal is HpickS.
We prove the intermediate claim HaNotC: a ∉ C.
Assume HaC: a ∈ C.
We prove the intermediate claim HaS: a ∈ S.
An exact proof term for the current goal is (HCsubS a HaC).
We prove the intermediate claim HaNotAB: a ∉ (A ∪ B).
An exact proof term for the current goal is (setminusE2 X (A ∪ B) a HaS).
We prove the intermediate claim HaAB: a ∈ (A ∪ B).
An exact proof term for the current goal is (binunionI1 A B a HaA).
An exact proof term for the current goal is (HaNotAB HaAB).
We prove the intermediate claim HbNotC: b ∉ C.
Assume HbC: b ∈ C.
We prove the intermediate claim HbS: b ∈ S.
An exact proof term for the current goal is (HCsubS b HbC).
We prove the intermediate claim HbNotAB: b ∉ (A ∪ B).
An exact proof term for the current goal is (setminusE2 X (A ∪ B) b HbS).
We prove the intermediate claim HbAB: b ∈ (A ∪ B).
An exact proof term for the current goal is (binunionI2 A B b HbB).
An exact proof term for the current goal is (HbNotAB HbAB).
We prove the intermediate claim HaY: a ∈ Y.
Apply setminusI to the current goal.
An exact proof term for the current goal is HaX.
An exact proof term for the current goal is HaNotC.
We prove the intermediate claim HbY: b ∈ Y.
Apply setminusI to the current goal.
An exact proof term for the current goal is HbX.
An exact proof term for the current goal is HbNotC.
We prove the intermediate claim HxCompA: x ∈ component_of Y Ty a.
rewrite the current goal using HDeq (from right to left).
An exact proof term for the current goal is HxD.
We prove the intermediate claim HxCompB: x ∈ component_of Y Ty b.
rewrite the current goal using HEeq (from right to left).
An exact proof term for the current goal is HxE.
We prove the intermediate claim HcompEqA: component_of Y Ty x = component_of Y Ty a.
An exact proof term for the current goal is (component_of_eq_if_in Y Ty a x HTy HaY HxCompA).
We prove the intermediate claim HcompEqB: component_of Y Ty x = component_of Y Ty b.
An exact proof term for the current goal is (component_of_eq_if_in Y Ty b x HTy HbY HxCompB).
We prove the intermediate claim HaInCompX: a ∈ component_of Y Ty x.
We prove the intermediate claim HaCompA: a ∈ component_of Y Ty a.
An exact proof term for the current goal is (point_in_component Y Ty a HTy HaY).
rewrite the current goal using HcompEqA (from left to right).
An exact proof term for the current goal is HaCompA.
We prove the intermediate claim HbInCompX: b ∈ component_of Y Ty x.
We prove the intermediate claim HbCompB: b ∈ component_of Y Ty b.
An exact proof term for the current goal is (point_in_component Y Ty b HTy HbY).
rewrite the current goal using HcompEqB (from left to right).
An exact proof term for the current goal is HbCompB.
We prove the intermediate claim HnoBoth: ¬ (∃a0 b0 : set, a0 ∈ A ∧ b0 ∈ B ∧ a0 ∈ component_of Y Ty x ∧ b0 ∈ component_of Y Ty x).
We prove the intermediate claim HxY: x ∈ Y.
An exact proof term for the current goal is (SepE1 Y (λy0 : set ⇒ ∃C0 : set, connected_space C0 (subspace_topology Y Ty C0) ∧ a ∈ C0 ∧ y0 ∈ C0) x HxCompA).
An exact proof term for the current goal is (ex32_8c_component_of_X_minus_C_not_both X (order_topology X) A B C HlinOrd HAcl HBcl HAB Hchoice HCcl x HxY).
We prove the intermediate claim HexBoth: ∃a0 b0 : set, a0 ∈ A ∧ b0 ∈ B ∧ a0 ∈ component_of Y Ty x ∧ b0 ∈ component_of Y Ty x.
We use a to witness the existential quantifier.
We use b to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HaA.
An exact proof term for the current goal is HbB.
An exact proof term for the current goal is HaInCompX.
An exact proof term for the current goal is HbInCompX.
Apply FalseE to the current goal.
An exact proof term for the current goal is (HnoBoth HexBoth).
Let x be given.
Assume Hx: x ∈ Empty.
An exact proof term for the current goal is (EmptyE x Hx (x ∈ U ∩ V)).
∎