Assume Hchoice: ∀W : set, (∃x : set, x ∈ (X ∖ (A ∪ B)) ∧ W = component_of (X ∖ (A ∪ B)) (subspace_topology X Tx (X ∖ (A ∪ B))) 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.

We will prove ¬ (∃a b : set, a ∈ A ∧ b ∈ B ∧ a ∈ component_of (X ∖ C) (subspace_topology X Tx (X ∖ C)) x ∧ b ∈ component_of (X ∖ C) (subspace_topology X Tx (X ∖ C)) x).

Assume HexAB: ∃a b : set, a ∈ A ∧ b ∈ B ∧ a ∈ component_of (X ∖ C) (subspace_topology X Tx (X ∖ C)) x ∧ b ∈ component_of (X ∖ C) (subspace_topology X Tx (X ∖ C)) x.

Apply (and4E (a ∈ A) (b ∈ B) (a ∈ component_of (X ∖ C) (subspace_topology X Tx (X ∖ C)) x) (b ∈ component_of (X ∖ C) (subspace_topology X Tx (X ∖ C)) x) HabPack) to the current goal.

We prove the intermediate claim HexW: ∃W : set, (∃y : set, y ∈ (X ∖ (A ∪ B)) ∧ W = component_of (X ∖ (A ∪ B)) (subspace_topology X Tx (X ∖ (A ∪ B))) y) ∧ (∃a0 b0 : set, a0 ∈ A ∧ b0 ∈ B ∧ order_rel X a0 b0 ∧ W = order_interval X a0 b0) ∧ W ⊆ component_of (X ∖ C) (subspace_topology X Tx (X ∖ C)) x.

An exact proof term for the current goal is (ex32_8c_find_interval_component_in_component X Tx A B C x a b Hlin HAcl HBcl HAB HCcl HaA HbB HxYC HaComp HbComp).

We prove the intermediate claim HWab: (∃y : set, y ∈ (X ∖ (A ∪ B)) ∧ W = component_of (X ∖ (A ∪ B)) (subspace_topology X Tx (X ∖ (A ∪ B))) y) ∧ (∃a0 b0 : set, a0 ∈ A ∧ b0 ∈ B ∧ order_rel X a0 b0 ∧ W = order_interval X a0 b0).

An exact proof term for the current goal is (andEL ((∃y : set, y ∈ (X ∖ (A ∪ B)) ∧ W = component_of (X ∖ (A ∪ B)) (subspace_topology X Tx (X ∖ (A ∪ B))) y) ∧ (∃a0 b0 : set, a0 ∈ A ∧ b0 ∈ B ∧ order_rel X a0 b0 ∧ W = order_interval X a0 b0)) (W ⊆ component_of (X ∖ C) (subspace_topology X Tx (X ∖ C)) x) HWpack).

We prove the intermediate claim HWsub: W ⊆ component_of (X ∖ C) (subspace_topology X Tx (X ∖ C)) x.

An exact proof term for the current goal is (andER ((∃y : set, y ∈ (X ∖ (A ∪ B)) ∧ W = component_of (X ∖ (A ∪ B)) (subspace_topology X Tx (X ∖ (A ∪ B))) y) ∧ (∃a0 b0 : set, a0 ∈ A ∧ b0 ∈ B ∧ order_rel X a0 b0 ∧ W = order_interval X a0 b0)) (W ⊆ component_of (X ∖ C) (subspace_topology X Tx (X ∖ C)) x) HWpack).

We prove the intermediate claim HWcomp: ∃y : set, y ∈ (X ∖ (A ∪ B)) ∧ W = component_of (X ∖ (A ∪ B)) (subspace_topology X Tx (X ∖ (A ∪ B))) y.

An exact proof term for the current goal is (andEL (∃y : set, y ∈ (X ∖ (A ∪ B)) ∧ W = component_of (X ∖ (A ∪ B)) (subspace_topology X Tx (X ∖ (A ∪ B))) y) (∃a0 b0 : set, a0 ∈ A ∧ b0 ∈ B ∧ order_rel X a0 b0 ∧ W = order_interval X a0 b0) HWab).

We prove the intermediate claim HWend: ∃a0 b0 : set, a0 ∈ A ∧ b0 ∈ B ∧ order_rel X a0 b0 ∧ W = order_interval X a0 b0.

An exact proof term for the current goal is (andER (∃y : set, y ∈ (X ∖ (A ∪ B)) ∧ W = component_of (X ∖ (A ∪ B)) (subspace_topology X Tx (X ∖ (A ∪ B))) y) (∃a0 b0 : set, a0 ∈ A ∧ b0 ∈ B ∧ order_rel X a0 b0 ∧ W = order_interval X a0 b0) HWab).

We prove the intermediate claim HexcW: ∃cW : set, cW ∈ C ∧ cW ∈ W.

An exact proof term for the current goal is (Hchoice W HWcomp HWend).

An exact proof term for the current goal is (andEL (cW ∈ C) (cW ∈ W) HcWpack).

An exact proof term for the current goal is (andER (cW ∈ C) (cW ∈ W) HcWpack).

We prove the intermediate claim HcWComp: cW ∈ component_of (X ∖ C) (subspace_topology X Tx (X ∖ C)) x.

An exact proof term for the current goal is (HWsub cW HcWW).

An exact proof term for the current goal is (SepE1 (X ∖ C) (λy0 : set ⇒ ∃D : set, connected_space D (subspace_topology (X ∖ C) (subspace_topology X Tx (X ∖ C)) D) ∧ x ∈ D ∧ y0 ∈ D) cW HcWComp).

An exact proof term for the current goal is (setminusE2 X C cW HcWY).