Assume Hleft.

We prove the intermediate claim HABsub: A ∈ subspace_topology X Tx Y ∧ B ∈ subspace_topology X Tx Y.

An exact proof term for the current goal is (andEL (A ∈ subspace_topology X Tx Y ∧ B ∈ subspace_topology X Tx Y) (separation_of Y A B) Hleft).

We prove the intermediate claim HAinTy: A ∈ subspace_topology X Tx Y.

An exact proof term for the current goal is (andEL (A ∈ subspace_topology X Tx Y) (B ∈ subspace_topology X Tx Y) HABsub).

We prove the intermediate claim HBinTy: B ∈ subspace_topology X Tx Y.

An exact proof term for the current goal is (andER (A ∈ subspace_topology X Tx Y) (B ∈ subspace_topology X Tx Y) HABsub).

We prove the intermediate claim Hsep: separation_of Y A B.

An exact proof term for the current goal is (andER (A ∈ subspace_topology X Tx Y ∧ B ∈ subspace_topology X Tx Y) (separation_of Y A B) Hleft).

We will prove separation_of Y A B ∧ ¬ (∃b : set, b ∈ B ∧ limit_point_of X Tx A b) ∧ ¬ (∃a : set, a ∈ A ∧ limit_point_of X Tx B a).

Apply andI to the current goal.

An exact proof term for the current goal is Hsep.

We will prove ¬ (∃b : set, b ∈ B ∧ limit_point_of X Tx A b).

Assume Hex: ∃b : set, b ∈ B ∧ limit_point_of X Tx A b.

We will prove False.

Apply Hex to the current goal.

Let b be given.

Assume Hbconj.

We prove the intermediate claim HbB: b ∈ B.

An exact proof term for the current goal is (andEL (b ∈ B) (limit_point_of X Tx A b) Hbconj).

We prove the intermediate claim HLP: limit_point_of X Tx A b.

An exact proof term for the current goal is (andER (b ∈ B) (limit_point_of X Tx A b) Hbconj).

We prove the intermediate claim HexV: ∃V ∈ Tx, B = V ∩ Y.

An exact proof term for the current goal is (subspace_topologyE X Tx Y B HBinTy).

Apply HexV to the current goal.

Let V be given.

Assume HVpair.

We prove the intermediate claim HVTx: V ∈ Tx.

An exact proof term for the current goal is (andEL (V ∈ Tx) (B = V ∩ Y) HVpair).

We prove the intermediate claim HBeq: B = V ∩ Y.

An exact proof term for the current goal is (andER (V ∈ Tx) (B = V ∩ Y) HVpair).

We prove the intermediate claim Hpart1: ((((A ∈ 𝒫 Y ∧ B ∈ 𝒫 Y) ∧ A ∩ B = Empty) ∧ A ≠ Empty) ∧ B ≠ Empty).

An exact proof term for the current goal is (andEL ((((A ∈ 𝒫 Y ∧ B ∈ 𝒫 Y) ∧ A ∩ B = Empty) ∧ A ≠ Empty) ∧ B ≠ Empty) (A ∪ B = Y) Hsep).

We prove the intermediate claim HAux: (((A ∈ 𝒫 Y ∧ B ∈ 𝒫 Y) ∧ A ∩ B = Empty) ∧ A ≠ Empty).

An exact proof term for the current goal is (andEL (((A ∈ 𝒫 Y ∧ B ∈ 𝒫 Y) ∧ A ∩ B = Empty) ∧ A ≠ Empty) (B ≠ Empty) Hpart1).

We prove the intermediate claim Hpowdisj: (A ∈ 𝒫 Y ∧ B ∈ 𝒫 Y) ∧ A ∩ B = Empty.

An exact proof term for the current goal is (andEL ((A ∈ 𝒫 Y ∧ B ∈ 𝒫 Y) ∧ A ∩ B = Empty) (A ≠ Empty) HAux).

We prove the intermediate claim Hpow: A ∈ 𝒫 Y ∧ B ∈ 𝒫 Y.

An exact proof term for the current goal is (andEL (A ∈ 𝒫 Y ∧ B ∈ 𝒫 Y) (A ∩ B = Empty) Hpowdisj).

We prove the intermediate claim Hdisj: A ∩ B = Empty.

An exact proof term for the current goal is (andER (A ∈ 𝒫 Y ∧ B ∈ 𝒫 Y) (A ∩ B = Empty) Hpowdisj).

We prove the intermediate claim HApowY: A ∈ 𝒫 Y.

An exact proof term for the current goal is (andEL (A ∈ 𝒫 Y) (B ∈ 𝒫 Y) Hpow).

We prove the intermediate claim HBpowY: B ∈ 𝒫 Y.

An exact proof term for the current goal is (andER (A ∈ 𝒫 Y) (B ∈ 𝒫 Y) Hpow).

We prove the intermediate claim HAsubY: A ⊆ Y.

An exact proof term for the current goal is (PowerE Y A HApowY).

We prove the intermediate claim HBsubY: B ⊆ Y.

An exact proof term for the current goal is (PowerE Y B HBpowY).

We prove the intermediate claim HbVY: b ∈ V ∩ Y.

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

An exact proof term for the current goal is HbB.

We prove the intermediate claim HbV: b ∈ V.

An exact proof term for the current goal is (binintersectE1 V Y b HbVY).

We prove the intermediate claim HLPp: topology_on X Tx ∧ b ∈ X.

An exact proof term for the current goal is (andEL (topology_on X Tx ∧ b ∈ X) (∀U : set, U ∈ Tx → b ∈ U → ∃y : set, y ∈ A ∧ y ≠ b ∧ y ∈ U) HLP).

We prove the intermediate claim HLPcond: ∀U : set, U ∈ Tx → b ∈ U → ∃y : set, y ∈ A ∧ y ≠ b ∧ y ∈ U.

An exact proof term for the current goal is (andER (topology_on X Tx ∧ b ∈ X) (∀U : set, U ∈ Tx → b ∈ U → ∃y : set, y ∈ A ∧ y ≠ b ∧ y ∈ U) HLP).

We prove the intermediate claim Hexy: ∃y : set, y ∈ A ∧ y ≠ b ∧ y ∈ V.

An exact proof term for the current goal is (HLPcond V HVTx HbV).

Apply Hexy to the current goal.

Let y be given.

Assume Hyconj.

We prove the intermediate claim HyAB: y ∈ A ∧ y ≠ b.

An exact proof term for the current goal is (andEL (y ∈ A ∧ y ≠ b) (y ∈ V) Hyconj).

We prove the intermediate claim HyA: y ∈ A.

An exact proof term for the current goal is (andEL (y ∈ A) (y ≠ b) HyAB).

We prove the intermediate claim HyV: y ∈ V.

An exact proof term for the current goal is (andER (y ∈ A ∧ y ≠ b) (y ∈ V) Hyconj).

We prove the intermediate claim HyY: y ∈ Y.

An exact proof term for the current goal is (HAsubY y HyA).

We prove the intermediate claim HyB: y ∈ B.

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

An exact proof term for the current goal is (binintersectI V Y y HyV HyY).

We prove the intermediate claim HyAB2: y ∈ A ∩ B.

An exact proof term for the current goal is (binintersectI A B y HyA HyB).

We prove the intermediate claim HyE: y ∈ Empty.

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

An exact proof term for the current goal is HyAB2.

An exact proof term for the current goal is (EmptyE y HyE).

We will prove ¬ (∃a : set, a ∈ A ∧ limit_point_of X Tx B a).

Assume Hex: ∃a : set, a ∈ A ∧ limit_point_of X Tx B a.

We will prove False.

Apply Hex to the current goal.

Let a be given.

Assume Haconj.

We prove the intermediate claim HaA: a ∈ A.

An exact proof term for the current goal is (andEL (a ∈ A) (limit_point_of X Tx B a) Haconj).

We prove the intermediate claim HLP: limit_point_of X Tx B a.

An exact proof term for the current goal is (andER (a ∈ A) (limit_point_of X Tx B a) Haconj).

We prove the intermediate claim HexU: ∃U ∈ Tx, A = U ∩ Y.

An exact proof term for the current goal is (subspace_topologyE X Tx Y A HAinTy).

Apply HexU to the current goal.

Let U be given.

Assume HUpair.

We prove the intermediate claim HUTx: U ∈ Tx.

An exact proof term for the current goal is (andEL (U ∈ Tx) (A = U ∩ Y) HUpair).

We prove the intermediate claim HAeq: A = U ∩ Y.

An exact proof term for the current goal is (andER (U ∈ Tx) (A = U ∩ Y) HUpair).

We prove the intermediate claim Hpart1: ((((A ∈ 𝒫 Y ∧ B ∈ 𝒫 Y) ∧ A ∩ B = Empty) ∧ A ≠ Empty) ∧ B ≠ Empty).

An exact proof term for the current goal is (andEL ((((A ∈ 𝒫 Y ∧ B ∈ 𝒫 Y) ∧ A ∩ B = Empty) ∧ A ≠ Empty) ∧ B ≠ Empty) (A ∪ B = Y) Hsep).

We prove the intermediate claim HAux: (((A ∈ 𝒫 Y ∧ B ∈ 𝒫 Y) ∧ A ∩ B = Empty) ∧ A ≠ Empty).

An exact proof term for the current goal is (andEL (((A ∈ 𝒫 Y ∧ B ∈ 𝒫 Y) ∧ A ∩ B = Empty) ∧ A ≠ Empty) (B ≠ Empty) Hpart1).

We prove the intermediate claim Hpowdisj: (A ∈ 𝒫 Y ∧ B ∈ 𝒫 Y) ∧ A ∩ B = Empty.

An exact proof term for the current goal is (andEL ((A ∈ 𝒫 Y ∧ B ∈ 𝒫 Y) ∧ A ∩ B = Empty) (A ≠ Empty) HAux).

We prove the intermediate claim Hpow: A ∈ 𝒫 Y ∧ B ∈ 𝒫 Y.

An exact proof term for the current goal is (andEL (A ∈ 𝒫 Y ∧ B ∈ 𝒫 Y) (A ∩ B = Empty) Hpowdisj).

We prove the intermediate claim Hdisj: A ∩ B = Empty.

An exact proof term for the current goal is (andER (A ∈ 𝒫 Y ∧ B ∈ 𝒫 Y) (A ∩ B = Empty) Hpowdisj).

We prove the intermediate claim HApowY: A ∈ 𝒫 Y.

An exact proof term for the current goal is (andEL (A ∈ 𝒫 Y) (B ∈ 𝒫 Y) Hpow).

We prove the intermediate claim HBpowY: B ∈ 𝒫 Y.

An exact proof term for the current goal is (andER (A ∈ 𝒫 Y) (B ∈ 𝒫 Y) Hpow).

We prove the intermediate claim HAsubY: A ⊆ Y.

An exact proof term for the current goal is (PowerE Y A HApowY).

We prove the intermediate claim HBsubY: B ⊆ Y.

An exact proof term for the current goal is (PowerE Y B HBpowY).

We prove the intermediate claim HaUY: a ∈ U ∩ Y.

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

An exact proof term for the current goal is HaA.

We prove the intermediate claim HaU: a ∈ U.

An exact proof term for the current goal is (binintersectE1 U Y a HaUY).

We prove the intermediate claim HLPcond: ∀V0 : set, V0 ∈ Tx → a ∈ V0 → ∃y : set, y ∈ B ∧ y ≠ a ∧ y ∈ V0.

An exact proof term for the current goal is (andER (topology_on X Tx ∧ a ∈ X) (∀V0 : set, V0 ∈ Tx → a ∈ V0 → ∃y : set, y ∈ B ∧ y ≠ a ∧ y ∈ V0) HLP).

We prove the intermediate claim Hexy: ∃y : set, y ∈ B ∧ y ≠ a ∧ y ∈ U.

An exact proof term for the current goal is (HLPcond U HUTx HaU).

Apply Hexy to the current goal.

Let y be given.

Assume Hyconj.

We prove the intermediate claim HyBA: y ∈ B ∧ y ≠ a.

An exact proof term for the current goal is (andEL (y ∈ B ∧ y ≠ a) (y ∈ U) Hyconj).

We prove the intermediate claim HyB: y ∈ B.

An exact proof term for the current goal is (andEL (y ∈ B) (y ≠ a) HyBA).

We prove the intermediate claim HyU: y ∈ U.

An exact proof term for the current goal is (andER (y ∈ B ∧ y ≠ a) (y ∈ U) Hyconj).

We prove the intermediate claim HyY: y ∈ Y.

An exact proof term for the current goal is (HBsubY y HyB).

We prove the intermediate claim HyA2: y ∈ A.

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

An exact proof term for the current goal is (binintersectI U Y y HyU HyY).

We prove the intermediate claim HyAB2: y ∈ A ∩ B.

An exact proof term for the current goal is (binintersectI A B y HyA2 HyB).

We prove the intermediate claim HyE: y ∈ Empty.

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

An exact proof term for the current goal is HyAB2.

An exact proof term for the current goal is (EmptyE y HyE).

Assume Hright.

We prove the intermediate claim Htmp: separation_of Y A B ∧ ¬ (∃b : set, b ∈ B ∧ limit_point_of X Tx A b).

An exact proof term for the current goal is (andEL (separation_of Y A B ∧ ¬ (∃b : set, b ∈ B ∧ limit_point_of X Tx A b)) (¬ (∃a : set, a ∈ A ∧ limit_point_of X Tx B a)) Hright).

We prove the intermediate claim Hsep: separation_of Y A B.

An exact proof term for the current goal is (andEL (separation_of Y A B) (¬ (∃b : set, b ∈ B ∧ limit_point_of X Tx A b)) Htmp).

We prove the intermediate claim HnoB: ¬ (∃b : set, b ∈ B ∧ limit_point_of X Tx A b).

An exact proof term for the current goal is (andER (separation_of Y A B) (¬ (∃b : set, b ∈ B ∧ limit_point_of X Tx A b)) Htmp).

We prove the intermediate claim HnoA: ¬ (∃a : set, a ∈ A ∧ limit_point_of X Tx B a).

An exact proof term for the current goal is (andER (separation_of Y A B ∧ ¬ (∃b : set, b ∈ B ∧ limit_point_of X Tx A b)) (¬ (∃a : set, a ∈ A ∧ limit_point_of X Tx B a)) Hright).

We prove the intermediate claim Hpart1: ((((A ∈ 𝒫 Y ∧ B ∈ 𝒫 Y) ∧ A ∩ B = Empty) ∧ A ≠ Empty) ∧ B ≠ Empty).

An exact proof term for the current goal is (andEL ((((A ∈ 𝒫 Y ∧ B ∈ 𝒫 Y) ∧ A ∩ B = Empty) ∧ A ≠ Empty) ∧ B ≠ Empty) (A ∪ B = Y) Hsep).

We prove the intermediate claim Hunion: A ∪ B = Y.

An exact proof term for the current goal is (andER ((((A ∈ 𝒫 Y ∧ B ∈ 𝒫 Y) ∧ A ∩ B = Empty) ∧ A ≠ Empty) ∧ B ≠ Empty) (A ∪ B = Y) Hsep).

We prove the intermediate claim HAux: (((A ∈ 𝒫 Y ∧ B ∈ 𝒫 Y) ∧ A ∩ B = Empty) ∧ A ≠ Empty).

An exact proof term for the current goal is (andEL (((A ∈ 𝒫 Y ∧ B ∈ 𝒫 Y) ∧ A ∩ B = Empty) ∧ A ≠ Empty) (B ≠ Empty) Hpart1).

We prove the intermediate claim Hpowdisj: (A ∈ 𝒫 Y ∧ B ∈ 𝒫 Y) ∧ A ∩ B = Empty.

An exact proof term for the current goal is (andEL ((A ∈ 𝒫 Y ∧ B ∈ 𝒫 Y) ∧ A ∩ B = Empty) (A ≠ Empty) HAux).

We prove the intermediate claim Hpow: A ∈ 𝒫 Y ∧ B ∈ 𝒫 Y.

An exact proof term for the current goal is (andEL (A ∈ 𝒫 Y ∧ B ∈ 𝒫 Y) (A ∩ B = Empty) Hpowdisj).

We prove the intermediate claim Hdisj: A ∩ B = Empty.

An exact proof term for the current goal is (andER (A ∈ 𝒫 Y ∧ B ∈ 𝒫 Y) (A ∩ B = Empty) Hpowdisj).

We prove the intermediate claim HApowY: A ∈ 𝒫 Y.

An exact proof term for the current goal is (andEL (A ∈ 𝒫 Y) (B ∈ 𝒫 Y) Hpow).

We prove the intermediate claim HBpowY: B ∈ 𝒫 Y.

An exact proof term for the current goal is (andER (A ∈ 𝒫 Y) (B ∈ 𝒫 Y) Hpow).

We prove the intermediate claim HAsubY: A ⊆ Y.

An exact proof term for the current goal is (PowerE Y A HApowY).

We prove the intermediate claim HBsubY: B ⊆ Y.

An exact proof term for the current goal is (PowerE Y B HBpowY).

We prove the intermediate claim HtopY: topology_on Y (subspace_topology X Tx Y).

An exact proof term for the current goal is (subspace_topology_is_topology X Tx Y HTx HY).

We prove the intermediate claim HAopen_in: open_in Y (subspace_topology X Tx Y) A.

Apply (ex13_1_local_open_subset Y (subspace_topology X Tx Y) A HtopY) to the current goal.

Let x be given.

Assume HxA: x ∈ A.

We will prove ∃U ∈ subspace_topology X Tx Y, x ∈ U ∧ U ⊆ A.

We prove the intermediate claim HnotLP: ¬ (limit_point_of X Tx B x).

Assume HLP.

Apply HnoA to the current goal.

We use x to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HxA.

An exact proof term for the current goal is HLP.

We prove the intermediate claim HxY: x ∈ Y.

An exact proof term for the current goal is (HAsubY x HxA).

We prove the intermediate claim HxX: x ∈ X.

An exact proof term for the current goal is (HY x HxY).

We prove the intermediate claim HnotForall: ¬ (∀W : set, W ∈ Tx → x ∈ W → ∃y : set, y ∈ B ∧ y ≠ x ∧ y ∈ W).

Assume Hforall.

Apply HnotLP to the current goal.

We will prove topology_on X Tx ∧ x ∈ X ∧ ∀U : set, U ∈ Tx → x ∈ U → ∃y : set, y ∈ B ∧ y ≠ x ∧ y ∈ U.

Apply andI to the current goal.

An exact proof term for the current goal is HTx.

An exact proof term for the current goal is HxX.

An exact proof term for the current goal is Hforall.

We prove the intermediate claim HexW: ∃W : set, ¬ (W ∈ Tx → x ∈ W → ∃y : set, y ∈ B ∧ y ≠ x ∧ y ∈ W).

An exact proof term for the current goal is (not_all_ex_demorgan_i (λW : set ⇒ W ∈ Tx → x ∈ W → ∃y : set, y ∈ B ∧ y ≠ x ∧ y ∈ W) HnotForall).

Apply HexW to the current goal.

Let W be given.

Assume HnImp.

We prove the intermediate claim HWTx: W ∈ Tx.

Apply (xm (W ∈ Tx)) to the current goal.

Assume HW.

An exact proof term for the current goal is HW.

Assume HnotW.

Apply FalseE to the current goal.

Apply HnImp to the current goal.

Assume HW0: W ∈ Tx.

Assume HxW0: x ∈ W.

Apply FalseE to the current goal.

An exact proof term for the current goal is (HnotW HW0).

We prove the intermediate claim HxW: x ∈ W.

Apply (xm (x ∈ W)) to the current goal.

Assume Hx.

An exact proof term for the current goal is Hx.

Assume Hnotx.

Apply FalseE to the current goal.

Apply HnImp to the current goal.

Assume HW0: W ∈ Tx.

Assume HxW0: x ∈ W.

Apply FalseE to the current goal.

An exact proof term for the current goal is (Hnotx HxW0).

We prove the intermediate claim HnoY: ¬ (∃y : set, y ∈ B ∧ y ≠ x ∧ y ∈ W).

Assume Hexy.

Apply HnImp to the current goal.

Assume HW0: W ∈ Tx.

Assume HxW0: x ∈ W.

An exact proof term for the current goal is Hexy.

Set U to be the term W ∩ Y.

We use U to witness the existential quantifier.

Apply andI to the current goal.

We will prove U ∈ subspace_topology X Tx Y.

An exact proof term for the current goal is (subspace_topologyI X Tx Y W HWTx).

Apply andI to the current goal.

An exact proof term for the current goal is (binintersectI W Y x HxW HxY).

We will prove U ⊆ A.

Let t be given.

Assume Ht: t ∈ U.

We will prove t ∈ A.

We prove the intermediate claim HtY: t ∈ Y.

An exact proof term for the current goal is (binintersectE2 W Y t Ht).

We prove the intermediate claim HtnotB: t ∉ B.

Assume HtB: t ∈ B.

Apply HnoY to the current goal.

We use t to witness the existential quantifier.

We will prove (t ∈ B ∧ t ≠ x) ∧ t ∈ W.

Apply andI to the current goal.

An exact proof term for the current goal is HtB.

Assume Heq: t = x.

We prove the intermediate claim HxB: x ∈ B.

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

An exact proof term for the current goal is HtB.

We prove the intermediate claim HxAB: x ∈ A ∩ B.

An exact proof term for the current goal is (binintersectI A B x HxA HxB).

We prove the intermediate claim HxE: x ∈ Empty.

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

An exact proof term for the current goal is HxAB.

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

An exact proof term for the current goal is (binintersectE1 W Y t Ht).

We prove the intermediate claim HtAB: t ∈ A ∪ B.

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

An exact proof term for the current goal is HtY.

Apply (binunionE A B t HtAB) to the current goal.

Assume HtA.

An exact proof term for the current goal is HtA.

Assume HtB.

Apply FalseE to the current goal.

An exact proof term for the current goal is (HtnotB HtB).

We prove the intermediate claim HATy: A ∈ subspace_topology X Tx Y.

An exact proof term for the current goal is (andER (topology_on Y (subspace_topology X Tx Y)) (A ∈ subspace_topology X Tx Y) HAopen_in).

We prove the intermediate claim HBopen_in: open_in Y (subspace_topology X Tx Y) B.

Apply (ex13_1_local_open_subset Y (subspace_topology X Tx Y) B HtopY) to the current goal.

Let x be given.

Assume HxB: x ∈ B.

We will prove ∃U ∈ subspace_topology X Tx Y, x ∈ U ∧ U ⊆ B.

We prove the intermediate claim HnotLP: ¬ (limit_point_of X Tx A x).

Assume HLP.

Apply HnoB to the current goal.

We use x to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HxB.

An exact proof term for the current goal is HLP.

We prove the intermediate claim HxY: x ∈ Y.

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

We prove the intermediate claim HxX: x ∈ X.

An exact proof term for the current goal is (HY x HxY).

We prove the intermediate claim HnotForall: ¬ (∀W : set, W ∈ Tx → x ∈ W → ∃y : set, y ∈ A ∧ y ≠ x ∧ y ∈ W).

Assume Hforall.

Apply HnotLP to the current goal.

We will prove topology_on X Tx ∧ x ∈ X ∧ ∀U : set, U ∈ Tx → x ∈ U → ∃y : set, y ∈ A ∧ y ≠ x ∧ y ∈ U.

Apply andI to the current goal.

An exact proof term for the current goal is HTx.

An exact proof term for the current goal is HxX.

An exact proof term for the current goal is Hforall.

We prove the intermediate claim HexW: ∃W : set, ¬ (W ∈ Tx → x ∈ W → ∃y : set, y ∈ A ∧ y ≠ x ∧ y ∈ W).

An exact proof term for the current goal is (not_all_ex_demorgan_i (λW : set ⇒ W ∈ Tx → x ∈ W → ∃y : set, y ∈ A ∧ y ≠ x ∧ y ∈ W) HnotForall).

Apply HexW to the current goal.

Let W be given.

Assume HnImp.

We prove the intermediate claim HWTx: W ∈ Tx.

Apply (xm (W ∈ Tx)) to the current goal.

Assume HW.

An exact proof term for the current goal is HW.

Assume HnotW.

Apply FalseE to the current goal.

Apply HnImp to the current goal.

Assume HW0: W ∈ Tx.

Assume HxW0: x ∈ W.

Apply FalseE to the current goal.

An exact proof term for the current goal is (HnotW HW0).

We prove the intermediate claim HxW: x ∈ W.

Apply (xm (x ∈ W)) to the current goal.

Assume Hx.

An exact proof term for the current goal is Hx.

Assume Hnotx.

Apply FalseE to the current goal.

Apply HnImp to the current goal.

Assume HW0: W ∈ Tx.

Assume HxW0: x ∈ W.

Apply FalseE to the current goal.

An exact proof term for the current goal is (Hnotx HxW0).

We prove the intermediate claim HnoY: ¬ (∃y : set, y ∈ A ∧ y ≠ x ∧ y ∈ W).

Assume Hexy.

Apply HnImp to the current goal.

Assume HW0: W ∈ Tx.

Assume HxW0: x ∈ W.

An exact proof term for the current goal is Hexy.

Set U to be the term W ∩ Y.

We use U to witness the existential quantifier.

Apply andI to the current goal.

We will prove U ∈ subspace_topology X Tx Y.

An exact proof term for the current goal is (subspace_topologyI X Tx Y W HWTx).

Apply andI to the current goal.

An exact proof term for the current goal is (binintersectI W Y x HxW HxY).

We will prove U ⊆ B.

Let t be given.

Assume Ht: t ∈ U.

We will prove t ∈ B.

We prove the intermediate claim HtY: t ∈ Y.

An exact proof term for the current goal is (binintersectE2 W Y t Ht).

We prove the intermediate claim HtnotA: t ∉ A.

Assume HtA: t ∈ A.

Apply HnoY to the current goal.

We use t to witness the existential quantifier.

We will prove (t ∈ A ∧ t ≠ x) ∧ t ∈ W.

Apply andI to the current goal.

An exact proof term for the current goal is HtA.

Assume Heq: t = x.

We prove the intermediate claim HxA: x ∈ A.

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

An exact proof term for the current goal is HtA.

We prove the intermediate claim HxAB: x ∈ A ∩ B.

An exact proof term for the current goal is (binintersectI A B x HxA HxB).

We prove the intermediate claim HxE: x ∈ Empty.

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

An exact proof term for the current goal is HxAB.

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

An exact proof term for the current goal is (binintersectE1 W Y t Ht).

We prove the intermediate claim HtAB: t ∈ A ∪ B.

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

An exact proof term for the current goal is HtY.

Apply (binunionE A B t HtAB) to the current goal.

Assume HtA.

Apply FalseE to the current goal.

An exact proof term for the current goal is (HtnotA HtA).

Assume HtB.

An exact proof term for the current goal is HtB.

We prove the intermediate claim HBTy: B ∈ subspace_topology X Tx Y.

An exact proof term for the current goal is (andER (topology_on Y (subspace_topology X Tx Y)) (B ∈ subspace_topology X Tx Y) HBopen_in).

We will prove (A ∈ subspace_topology X Tx Y ∧ B ∈ subspace_topology X Tx Y) ∧ separation_of Y A B.

Apply andI to the current goal.

An exact proof term for the current goal is HATy.

An exact proof term for the current goal is HBTy.

An exact proof term for the current goal is Hsep.