Let X, Tx and x be given.
Assume HT1: T1_space X Tx.
Assume HxX: x ∈ X.
We will prove X ∖ {x} ∈ Tx.
We prove the intermediate claim Htop: topology_on X Tx.
An exact proof term for the current goal is (T1_space_topology X Tx HT1).
We prove the intermediate claim Hsing: closed_in X Tx {x}.
An exact proof term for the current goal is ((iffEL (T1_space X Tx) (∀z : set, z ∈ X → closed_in X Tx {z}) (lemma_T1_singletons_closed X Tx Htop) HT1) x HxX).
We prove the intermediate claim Hdef: topology_on X Tx ∧ ({x} ⊆ X ∧ ∃U ∈ Tx, {x} = X ∖ U).
An exact proof term for the current goal is Hsing.
We prove the intermediate claim Hsubex: {x} ⊆ X ∧ ∃U ∈ Tx, {x} = X ∖ U.
An exact proof term for the current goal is (andER (topology_on X Tx) ({x} ⊆ X ∧ ∃U ∈ Tx, {x} = X ∖ U) Hdef).
We prove the intermediate claim HexU: ∃U ∈ Tx, {x} = X ∖ U.
An exact proof term for the current goal is (andER ({x} ⊆ X) (∃U ∈ Tx, {x} = X ∖ U) Hsubex).
Apply HexU to the current goal.
Let U be given.
Assume HUeq.
We prove the intermediate claim HUinTx: U ∈ Tx.
An exact proof term for the current goal is (andEL (U ∈ Tx) ({x} = X ∖ U) HUeq).
We prove the intermediate claim Hxeq: {x} = X ∖ U.
An exact proof term for the current goal is (andER (U ∈ Tx) ({x} = X ∖ U) HUeq).
We prove the intermediate claim HxnotU: x ∉ U.
We prove the intermediate claim HxIn: x ∈ X ∖ U.
rewrite the current goal using Hxeq (from right to left).
An exact proof term for the current goal is (SingI x).
An exact proof term for the current goal is (setminusE2 X U x HxIn).
We prove the intermediate claim HeqU: U = X ∖ {x}.
Apply set_ext to the current goal.
Let z be given.
Assume HzU: z ∈ U.
We will prove z ∈ X ∖ {x}.
We prove the intermediate claim HzX: z ∈ X.
We prove the intermediate claim HTsub: Tx ⊆ 𝒫 X.
An exact proof term for the current goal is (topology_subset_axiom X Tx Htop).
We prove the intermediate claim HUPow: U ∈ 𝒫 X.
An exact proof term for the current goal is (HTsub U HUinTx).
We prove the intermediate claim HUsub: U ⊆ X.
An exact proof term for the current goal is (PowerE X U HUPow).
An exact proof term for the current goal is (HUsub z HzU).
Apply setminusI to the current goal.
An exact proof term for the current goal is HzX.
Assume HzSing: z ∈ {x}.
We prove the intermediate claim Hzeq: z = x.
An exact proof term for the current goal is (SingE x z HzSing).
We prove the intermediate claim HxU: x ∈ U.
We will prove x ∈ U.
rewrite the current goal using Hzeq (from right to left).
An exact proof term for the current goal is HzU.
An exact proof term for the current goal is (HxnotU HxU).
Let z be given.
Assume Hz: z ∈ X ∖ {x}.
We will prove z ∈ U.
Apply (xm (z ∈ U)) to the current goal.
Assume HzU: z ∈ U.
An exact proof term for the current goal is HzU.
Assume HznotU: z ∉ U.
We prove the intermediate claim HzIn: z ∈ X ∖ U.
An exact proof term for the current goal is (setminusI X U z (setminusE1 X {x} z Hz) HznotU).
We prove the intermediate claim HzSing: z ∈ {x}.
rewrite the current goal using Hxeq (from left to right).
An exact proof term for the current goal is HzIn.
We prove the intermediate claim Hfalse: False.
An exact proof term for the current goal is ((setminusE2 X {x} z Hz) HzSing).
Apply FalseE to the current goal.
An exact proof term for the current goal is Hfalse.
rewrite the current goal using HeqU (from right to left).
An exact proof term for the current goal is HUinTx.
∎