Set X0 to be the term {0} ∪ {1}.
Set Tx0 to be the term indiscrete_topology X0.
Set A0 to be the term X0.
Set B0 to be the term {0}.
We use X0 to witness the existential quantifier.
We use Tx0 to witness the existential quantifier.
We use A0 to witness the existential quantifier.
We use B0 to witness the existential quantifier.
We will prove topology_on X0 Tx0 ∧ A0 ⊆ X0 ∧ B0 ⊆ X0 ∧ closure_of X0 Tx0 (A0 ∖ B0) ≠ (closure_of X0 Tx0 A0 ∖ closure_of X0 Tx0 B0).
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is (indiscrete_topology_on X0).
An exact proof term for the current goal is (Subq_ref X0).
Let x be given.
Assume Hx: x ∈ B0.
We will prove x ∈ X0.
We prove the intermediate claim Hxeq: x = 0.
An exact proof term for the current goal is (SingE 0 x Hx).
rewrite the current goal using Hxeq (from left to right).
An exact proof term for the current goal is (binunionI1 {0} {1} 0 (SingI 0)).
Assume Heq: closure_of X0 Tx0 (A0 ∖ B0) = (closure_of X0 Tx0 A0 ∖ closure_of X0 Tx0 B0).
We prove the intermediate claim H0X0: 0 ∈ X0.
An exact proof term for the current goal is (binunionI1 {0} {1} 0 (SingI 0)).
We prove the intermediate claim H0in_left: 0 ∈ closure_of X0 Tx0 (A0 ∖ B0).
Apply (iffER (0 ∈ closure_of X0 Tx0 (A0 ∖ B0)) (∀U ∈ Tx0, 0 ∈ U → U ∩ (A0 ∖ B0) ≠ Empty) (closure_characterization X0 Tx0 (A0 ∖ B0) 0 (indiscrete_topology_on X0) H0X0)) to the current goal.
Let U be given.
Assume HU: U ∈ Tx0.
Assume H0U: 0 ∈ U.
We will prove U ∩ (A0 ∖ B0) ≠ Empty.
We prove the intermediate claim HUcases: U = Empty ∨ U = X0.
We prove the intermediate claim HU': U ∈ indiscrete_topology X0.
An exact proof term for the current goal is HU.
An exact proof term for the current goal is (iffEL (U ∈ indiscrete_topology X0) (U = Empty ∨ U = X0) (indiscrete_open_iff X0 U) HU').
Apply HUcases to the current goal.
Assume HUe: U = Empty.
Apply FalseE to the current goal.
We prove the intermediate claim H0notU: 0 ∉ U.
rewrite the current goal using HUe (from left to right).
An exact proof term for the current goal is (EmptyE 0).
An exact proof term for the current goal is (H0notU H0U).
Assume HUX: U = X0.
rewrite the current goal using HUX (from left to right).
We prove the intermediate claim H1X0: 1 ∈ X0.
An exact proof term for the current goal is (binunionI2 {0} {1} 1 (SingI 1)).
We prove the intermediate claim H1notB0: 1 ∉ B0.
Assume H1B0: 1 ∈ B0.
We prove the intermediate claim H10: 1 = 0.
An exact proof term for the current goal is (SingE 0 1 H1B0).
An exact proof term for the current goal is (neq_1_0 H10).
We prove the intermediate claim H1in: 1 ∈ A0 ∖ B0.
Apply setminusI to the current goal.
An exact proof term for the current goal is H1X0.
An exact proof term for the current goal is H1notB0.
We prove the intermediate claim H1in_inter: 1 ∈ X0 ∩ (A0 ∖ B0).
An exact proof term for the current goal is (binintersectI X0 (A0 ∖ B0) 1 H1X0 H1in).
An exact proof term for the current goal is (elem_implies_nonempty (X0 ∩ (A0 ∖ B0)) 1 H1in_inter).
We prove the intermediate claim H0in_clB: 0 ∈ closure_of X0 Tx0 B0.
We prove the intermediate claim HB0sub: B0 ⊆ X0.
Let x be given.
Assume Hx: x ∈ B0.
We will prove x ∈ X0.
We prove the intermediate claim Hxeq: x = 0.
An exact proof term for the current goal is (SingE 0 x Hx).
rewrite the current goal using Hxeq (from left to right).
An exact proof term for the current goal is (binunionI1 {0} {1} 0 (SingI 0)).
An exact proof term for the current goal is (subset_of_closure X0 Tx0 B0 (indiscrete_topology_on X0) HB0sub 0 (SingI 0)).
We prove the intermediate claim H0not_right: 0 ∉ (closure_of X0 Tx0 A0 ∖ closure_of X0 Tx0 B0).
Assume H0R: 0 ∈ (closure_of X0 Tx0 A0 ∖ closure_of X0 Tx0 B0).
We prove the intermediate claim H0not_clB: 0 ∉ closure_of X0 Tx0 B0.
An exact proof term for the current goal is (setminusE2 (closure_of X0 Tx0 A0) (closure_of X0 Tx0 B0) 0 H0R).
An exact proof term for the current goal is (H0not_clB H0in_clB).
Apply H0not_right to the current goal.
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is H0in_left.
∎