We will prove Y ⊆ X ∧ ∃U ∈ Tx, Y = X ∖ U.

Apply andI to the current goal.

An exact proof term for the current goal is HYsub.

We use (X ∖ Y) to witness the existential quantifier.

Apply andI to the current goal.

Set UFam to be the term {U ∈ Tx|∃x0 : set, x0 ∈ X ∖ Y ∧ x0 ∈ U ∧ U ∩ Y = Empty}.

We prove the intermediate claim HUFamSub: UFam ⊆ Tx.

Let U be given.

Assume HU: U ∈ UFam.

An exact proof term for the current goal is (SepE1 Tx (λU0 : set ⇒ ∃x0 : set, x0 ∈ X ∖ Y ∧ x0 ∈ U0 ∧ U0 ∩ Y = Empty) U HU).

We prove the intermediate claim HUnionEq: ⋃ UFam = X ∖ Y.

Apply set_ext to the current goal.

Let z be given.

Assume Hz: z ∈ ⋃ UFam.

We will prove z ∈ X ∖ Y.

Apply (UnionE_impred UFam z Hz) to the current goal.

Let U be given.

Assume HzU: z ∈ U.

Assume HU: U ∈ UFam.

We prove the intermediate claim HUtx: U ∈ Tx.

An exact proof term for the current goal is (SepE1 Tx (λU0 : set ⇒ ∃x0 : set, x0 ∈ X ∖ Y ∧ x0 ∈ U0 ∧ U0 ∩ Y = Empty) U HU).

We prove the intermediate claim HUsubX: U ⊆ X.

An exact proof term for the current goal is (topology_elem_subset X Tx U HTx HUtx).

We prove the intermediate claim HzX: z ∈ X.

An exact proof term for the current goal is (HUsubX z HzU).

We prove the intermediate claim Hpred: ∃x0 : set, x0 ∈ X ∖ Y ∧ x0 ∈ U ∧ U ∩ Y = Empty.

An exact proof term for the current goal is (SepE2 Tx (λU0 : set ⇒ ∃x0 : set, x0 ∈ X ∖ Y ∧ x0 ∈ U0 ∧ U0 ∩ Y = Empty) U HU).

Apply Hpred to the current goal.

Let x0 be given.

Assume Hx0: x0 ∈ X ∖ Y ∧ x0 ∈ U ∧ U ∩ Y = Empty.

We prove the intermediate claim HUYempty: U ∩ Y = Empty.

An exact proof term for the current goal is (andER (x0 ∈ X ∖ Y ∧ x0 ∈ U) (U ∩ Y = Empty) Hx0).

We prove the intermediate claim HzNotY: z ∉ Y.

Assume HzY: z ∈ Y.

We prove the intermediate claim HzInt: z ∈ U ∩ Y.

An exact proof term for the current goal is (binintersectI U Y z HzU HzY).

We prove the intermediate claim HzEmpty: z ∈ Empty.

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

An exact proof term for the current goal is HzInt.

An exact proof term for the current goal is (EmptyE z HzEmpty False).

An exact proof term for the current goal is (setminusI X Y z HzX HzNotY).

Let z be given.

Assume Hz: z ∈ X ∖ Y.

We will prove z ∈ ⋃ UFam.

We prove the intermediate claim HzX: z ∈ X.

An exact proof term for the current goal is (setminusE1 X Y z Hz).

We prove the intermediate claim HzNotY: z ∉ Y.

An exact proof term for the current goal is (setminusE2 X Y z Hz).

We prove the intermediate claim HexUV: ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ z ∈ U ∧ Y ⊆ V ∧ U ∩ V = Empty.

An exact proof term for the current goal is (Hausdorff_separate_point_compact_set_aux X Tx Y z HH HYsub Hcomp HzX HzNotY).

Apply HexUV to the current goal.

Let U be given.

Assume HexV: ∃V : set, U ∈ Tx ∧ V ∈ Tx ∧ z ∈ U ∧ Y ⊆ V ∧ U ∩ V = Empty.

Apply HexV to the current goal.

Let V be given.

Assume Hconj: U ∈ Tx ∧ V ∈ Tx ∧ z ∈ U ∧ Y ⊆ V ∧ U ∩ V = Empty.

We prove the intermediate claim HconjA: ((U ∈ Tx ∧ V ∈ Tx) ∧ z ∈ U) ∧ Y ⊆ V.

An exact proof term for the current goal is (andEL (((U ∈ Tx ∧ V ∈ Tx) ∧ z ∈ U) ∧ Y ⊆ V) (U ∩ V = Empty) Hconj).

We prove the intermediate claim HUVempty: U ∩ V = Empty.

An exact proof term for the current goal is (andER (((U ∈ Tx ∧ V ∈ Tx) ∧ z ∈ U) ∧ Y ⊆ V) (U ∩ V = Empty) Hconj).

We prove the intermediate claim HUVz: (U ∈ Tx ∧ V ∈ Tx) ∧ z ∈ U.

An exact proof term for the current goal is (andEL ((U ∈ Tx ∧ V ∈ Tx) ∧ z ∈ U) (Y ⊆ V) HconjA).

We prove the intermediate claim HUtx: U ∈ Tx.

An exact proof term for the current goal is (andEL (U ∈ Tx) (V ∈ Tx) (andEL (U ∈ Tx ∧ V ∈ Tx) (z ∈ U) HUVz)).

We prove the intermediate claim HzU: z ∈ U.

An exact proof term for the current goal is (andER (U ∈ Tx ∧ V ∈ Tx) (z ∈ U) HUVz).

We prove the intermediate claim HYsubV: Y ⊆ V.

An exact proof term for the current goal is (andER ((U ∈ Tx ∧ V ∈ Tx) ∧ z ∈ U) (Y ⊆ V) HconjA).

We prove the intermediate claim HUYsub: U ∩ Y ⊆ U ∩ V.

Let t be given.

Assume Ht: t ∈ U ∩ Y.

We will prove t ∈ U ∩ V.

We prove the intermediate claim HtU: t ∈ U.

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

We prove the intermediate claim HtY: t ∈ Y.

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

We prove the intermediate claim HtV: t ∈ V.

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

An exact proof term for the current goal is (binintersectI U V t HtU HtV).

We prove the intermediate claim HUYempty: U ∩ Y = Empty.

Apply Empty_Subq_eq to the current goal.

Let t be given.

Assume Ht: t ∈ U ∩ Y.

We will prove False.

We prove the intermediate claim HtUV: t ∈ U ∩ V.

An exact proof term for the current goal is (HUYsub t Ht).

We prove the intermediate claim HtEmpty: t ∈ Empty.

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

An exact proof term for the current goal is HtUV.

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

We prove the intermediate claim HzXY: z ∈ X ∖ Y.

An exact proof term for the current goal is (setminusI X Y z HzX HzNotY).

We prove the intermediate claim HUinUFam: U ∈ UFam.

Apply (SepI Tx (λU0 : set ⇒ ∃x0 : set, x0 ∈ X ∖ Y ∧ x0 ∈ U0 ∧ U0 ∩ Y = Empty) U HUtx) to the current goal.

We use z to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HzXY.

An exact proof term for the current goal is HzU.

An exact proof term for the current goal is HUYempty.

An exact proof term for the current goal is (UnionI UFam z U HzU HUinUFam).

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

An exact proof term for the current goal is (topology_union_closed X Tx UFam HTx HUFamSub).

Use symmetry.

An exact proof term for the current goal is (setminus_setminus_eq X Y HYsub).