Assume HnotYcC: ¬ (Y ⊆ C).

Apply (xm (Y ⊆ D)) to the current goal.

Assume HYD: Y ⊆ D.

Apply orIR to the current goal.

An exact proof term for the current goal is HYD.

Assume HnotYcD: ¬ (Y ⊆ D).

We prove the intermediate claim HexYnotC: ∃y : set, y ∈ Y ∧ y ∉ C.

We prove the intermediate claim Hex: ∃y : set, ¬ (y ∈ Y → y ∈ C).

An exact proof term for the current goal is (not_all_ex_demorgan_i (λy : set ⇒ y ∈ Y → y ∈ C) HnotYcC).

Apply Hex to the current goal.

Let y be given.

Assume Hnotimp.

We prove the intermediate claim HyY: y ∈ Y.

Apply (xm (y ∈ Y)) to the current goal.

Assume HyY.

An exact proof term for the current goal is HyY.

Assume HyNotY.

Apply FalseE to the current goal.

Apply Hnotimp to the current goal.

Assume HyY: y ∈ Y.

Apply FalseE to the current goal.

An exact proof term for the current goal is (HyNotY HyY).

We prove the intermediate claim HyNotC: y ∉ C.

Assume HyC: y ∈ C.

Apply Hnotimp to the current goal.

Assume _: y ∈ Y.

An exact proof term for the current goal is HyC.

We use y to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HyY.

An exact proof term for the current goal is HyNotC.

Apply HexYnotC to the current goal.

Let yD be given.

Assume HyDpair.

We prove the intermediate claim HyDY: yD ∈ Y.

An exact proof term for the current goal is (andEL (yD ∈ Y) (yD ∉ C) HyDpair).

We prove the intermediate claim HyDnotC: yD ∉ C.

An exact proof term for the current goal is (andER (yD ∈ Y) (yD ∉ C) HyDpair).

We prove the intermediate claim Hsep_left: ((((C ∈ 𝒫 X ∧ D ∈ 𝒫 X) ∧ C ∩ D = Empty) ∧ C ≠ Empty) ∧ D ≠ Empty).

An exact proof term for the current goal is (andEL ((((C ∈ 𝒫 X ∧ D ∈ 𝒫 X) ∧ C ∩ D = Empty) ∧ C ≠ Empty) ∧ D ≠ Empty) (C ∪ D = X) Hsep).

We prove the intermediate claim Hsep_pow_disj: (C ∈ 𝒫 X ∧ D ∈ 𝒫 X) ∧ C ∩ D = Empty.

An exact proof term for the current goal is (andEL ((C ∈ 𝒫 X ∧ D ∈ 𝒫 X) ∧ C ∩ D = Empty) (C ≠ Empty) (andEL (((C ∈ 𝒫 X ∧ D ∈ 𝒫 X) ∧ C ∩ D = Empty) ∧ C ≠ Empty) (D ≠ Empty) Hsep_left)).

We prove the intermediate claim HCpow: C ∈ 𝒫 X.

An exact proof term for the current goal is (andEL (C ∈ 𝒫 X) (D ∈ 𝒫 X) (andEL (C ∈ 𝒫 X ∧ D ∈ 𝒫 X) (C ∩ D = Empty) Hsep_pow_disj)).

We prove the intermediate claim HDpow: D ∈ 𝒫 X.

An exact proof term for the current goal is (andER (C ∈ 𝒫 X) (D ∈ 𝒫 X) (andEL (C ∈ 𝒫 X ∧ D ∈ 𝒫 X) (C ∩ D = Empty) Hsep_pow_disj)).

We prove the intermediate claim HCsubX: C ⊆ X.

An exact proof term for the current goal is (PowerE X C HCpow).

We prove the intermediate claim HDsubX: D ⊆ X.

An exact proof term for the current goal is (PowerE X D HDpow).

We prove the intermediate claim HunionCD: C ∪ D = X.

An exact proof term for the current goal is (andER ((((C ∈ 𝒫 X ∧ D ∈ 𝒫 X) ∧ C ∩ D = Empty) ∧ C ≠ Empty) ∧ D ≠ Empty) (C ∪ D = X) Hsep).

We prove the intermediate claim HyDX: yD ∈ X.

An exact proof term for the current goal is (HYX yD HyDY).

We prove the intermediate claim HyDinCD: yD ∈ C ∪ D.

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

An exact proof term for the current goal is HyDX.

We prove the intermediate claim HyDinD: yD ∈ D.

Apply (binunionE C D yD HyDinCD) to the current goal.

Assume HyDC: yD ∈ C.

Apply FalseE to the current goal.

An exact proof term for the current goal is (HyDnotC HyDC).

Assume HyDD: yD ∈ D.

An exact proof term for the current goal is HyDD.

We prove the intermediate claim HexYnotD: ∃y : set, y ∈ Y ∧ y ∉ D.

We prove the intermediate claim Hex: ∃y : set, ¬ (y ∈ Y → y ∈ D).

An exact proof term for the current goal is (not_all_ex_demorgan_i (λy : set ⇒ y ∈ Y → y ∈ D) HnotYcD).

Apply Hex to the current goal.

Let y be given.

Assume Hnotimp.

We prove the intermediate claim HyY: y ∈ Y.

Apply (xm (y ∈ Y)) to the current goal.

Assume HyY.

An exact proof term for the current goal is HyY.

Assume HyNotY.

Apply FalseE to the current goal.

Apply Hnotimp to the current goal.

Assume HyY: y ∈ Y.

Apply FalseE to the current goal.

An exact proof term for the current goal is (HyNotY HyY).

We prove the intermediate claim HyNotD: y ∉ D.

Assume HyD: y ∈ D.

Apply Hnotimp to the current goal.

Assume _: y ∈ Y.

An exact proof term for the current goal is HyD.

We use y to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HyY.

An exact proof term for the current goal is HyNotD.

Apply HexYnotD to the current goal.

Let yC be given.

Assume HyCpair.

We prove the intermediate claim HyCY: yC ∈ Y.

An exact proof term for the current goal is (andEL (yC ∈ Y) (yC ∉ D) HyCpair).

We prove the intermediate claim HyCnotD: yC ∉ D.

An exact proof term for the current goal is (andER (yC ∈ Y) (yC ∉ D) HyCpair).

We prove the intermediate claim HyCX: yC ∈ X.

An exact proof term for the current goal is (HYX yC HyCY).

We prove the intermediate claim HyCinCD: yC ∈ C ∪ D.

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

An exact proof term for the current goal is HyCX.

We prove the intermediate claim HyCinC: yC ∈ C.

Apply (binunionE C D yC HyCinCD) to the current goal.

Assume HyCC: yC ∈ C.

An exact proof term for the current goal is HyCC.

Assume HyCD: yC ∈ D.

Apply FalseE to the current goal.

An exact proof term for the current goal is (HyCnotD HyCD).

Set A to be the term C ∩ Y.

Set B to be the term D ∩ Y.

We prove the intermediate claim HAYsub: A ⊆ Y.

An exact proof term for the current goal is (binintersect_Subq_2 C Y).

We prove the intermediate claim HBYsub: B ⊆ Y.

An exact proof term for the current goal is (binintersect_Subq_2 D Y).

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

Apply (iffER (open_in Y (subspace_topology X Tx Y) A) (∃V ∈ Tx, A = V ∩ Y) (open_in_subspace_iff X Tx Y A HTx HYX HAYsub)) to the current goal.

We use C to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HC.

We will prove A = C ∩ Y.

Use reflexivity.

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

Apply (iffER (open_in Y (subspace_topology X Tx Y) B) (∃V ∈ Tx, B = V ∩ Y) (open_in_subspace_iff X Tx Y B HTx HYX HBYsub)) to the current goal.

We use D to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HD.

We will prove B = D ∩ Y.

Use reflexivity.

We prove the intermediate claim HAinSub: 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) HAopenY).

We prove the intermediate claim HBinSub: 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) HBopenY).

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

We will prove A ∈ 𝒫 Y ∧ B ∈ 𝒫 Y ∧ A ∩ B = Empty ∧ A ≠ Empty ∧ B ≠ Empty ∧ A ∪ B = Y.

Apply andI to the current goal.

We will prove ((((A ∈ 𝒫 Y ∧ B ∈ 𝒫 Y) ∧ A ∩ B = Empty) ∧ A ≠ Empty) ∧ B ≠ Empty).

Apply andI to the current goal.

We will prove (((A ∈ 𝒫 Y ∧ B ∈ 𝒫 Y) ∧ A ∩ B = Empty) ∧ A ≠ Empty).

Apply andI to the current goal.

We will prove (A ∈ 𝒫 Y ∧ B ∈ 𝒫 Y) ∧ A ∩ B = Empty.

Apply andI to the current goal.

We will prove A ∈ 𝒫 Y ∧ B ∈ 𝒫 Y.

Apply andI to the current goal.

An exact proof term for the current goal is (PowerI Y A HAYsub).

An exact proof term for the current goal is (PowerI Y B HBYsub).

We will prove A ∩ B = Empty.

Apply Empty_eq to the current goal.

Let t be given.

Assume Ht: t ∈ A ∩ B.

Apply (binintersectE A B t Ht) to the current goal.

Assume HtA: t ∈ A.

Assume HtB: t ∈ B.

We prove the intermediate claim HtC: t ∈ C.

An exact proof term for the current goal is (binintersectE1 C Y t HtA).

We prove the intermediate claim HtD: t ∈ D.

An exact proof term for the current goal is (binintersectE1 D Y t HtB).

We prove the intermediate claim HtCD: t ∈ C ∩ D.

An exact proof term for the current goal is (binintersectI C D t HtC HtD).

We prove the intermediate claim HCDdisj: C ∩ D = Empty.

An exact proof term for the current goal is (andER (C ∈ 𝒫 X ∧ D ∈ 𝒫 X) (C ∩ D = Empty) Hsep_pow_disj).

We prove the intermediate claim Hfalse: t ∈ Empty.

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

An exact proof term for the current goal is HtCD.

An exact proof term for the current goal is (EmptyE t Hfalse).

Assume Heq: A = Empty.

We prove the intermediate claim HyCA: yC ∈ A.

An exact proof term for the current goal is (binintersectI C Y yC HyCinC HyCY).

We prove the intermediate claim HyCEmpty: yC ∈ Empty.

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

An exact proof term for the current goal is HyCA.

An exact proof term for the current goal is (EmptyE yC HyCEmpty).

Assume Heq: B = Empty.

We prove the intermediate claim HyDB: yD ∈ B.

An exact proof term for the current goal is (binintersectI D Y yD HyDinD HyDY).

We prove the intermediate claim HyDEmpty: yD ∈ Empty.

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

An exact proof term for the current goal is HyDB.

An exact proof term for the current goal is (EmptyE yD HyDEmpty).

We will prove A ∪ B = Y.

Apply set_ext to the current goal.

Let t be given.

Assume Ht: t ∈ A ∪ B.

We will prove t ∈ Y.

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

Assume HtA: t ∈ A.

An exact proof term for the current goal is (binintersectE2 C Y t HtA).

Assume HtB: t ∈ B.

An exact proof term for the current goal is (binintersectE2 D Y t HtB).

Let t be given.

Assume HtY: t ∈ Y.

We will prove t ∈ A ∪ B.

We prove the intermediate claim HtX: t ∈ X.

An exact proof term for the current goal is (HYX t HtY).

We prove the intermediate claim HtCD: t ∈ C ∪ D.

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

An exact proof term for the current goal is HtX.

Apply (binunionE C D t HtCD) to the current goal.

Assume HtC: t ∈ C.

Apply binunionI1 to the current goal.

An exact proof term for the current goal is (binintersectI C Y t HtC HtY).

Assume HtD: t ∈ D.

Apply binunionI2 to the current goal.

An exact proof term for the current goal is (binintersectI D Y t HtD HtY).

We prove the intermediate claim HnosepY: ¬ (∃U V : set, U ∈ subspace_topology X Tx Y ∧ V ∈ subspace_topology X Tx Y ∧ separation_of Y U V).

An exact proof term for the current goal is (andER (topology_on Y (subspace_topology X Tx Y)) (¬ (∃U V : set, U ∈ subspace_topology X Tx Y ∧ V ∈ subspace_topology X Tx Y ∧ separation_of Y U V)) HY).

Apply FalseE to the current goal.

Apply HnosepY to the current goal.

We use A to witness the existential quantifier.

We use B to witness the existential quantifier.

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 HAinSub.

An exact proof term for the current goal is HBinSub.

An exact proof term for the current goal is HsepAB.