# Derivative of Derivative is Subset of Derivative in T1 Space

## Theorem

Let $T = \left({S, \tau}\right)$ be a $T_1$ topological space.

Let $A$ be a subset of $S$.

Then

- $A'' \subseteq A'$

where

- $A'$ denotes the derivative of $A$

## Proof

Let:

- $(1): \quad x \in A''$.

Aiming for a contradiction, suppose that $x \notin A'$.

Then by Characterization of Derivative by Open Sets there exists an open subset $G$ of $T$ such that:

- $(2): \quad x \in G$ and
- $(3): \quad \lnot \exists y: y \in A \cap G \land x \ne y$.

By definition of $T_1$ space:

- $\left\{{x}\right\}$ is closed.

Then by Open Set minus Closed Set is Open:

- $(4): \quad G \setminus \{x\}$ is open.

By $(1)$, $(2)$, and Characterization of Derivative by Open Sets there exists a point $y$ of $T$ such that:

- $(5): \quad y \in A' \cap G$ and
- $(6): \quad x \ne y$.

Then by definition of intersection:

- $y \in A'$.

Then by $(6)$ and definition of set difference:

- $(7): \quad y \in A' \setminus \{x\}$.

By definition of intersection and $(5)$:

- $y \in G$.

By $(6)$ and definition of singleton:

- $y \notin \left\{{x}\right\}$

Then by definition of set difference:

- $(8): \quad y \in G \setminus \{x\}$

We will prove:

- $(9): \quad G \cap \left({A \setminus \{x\}}\right) = \varnothing$

- Aiming for a contradiction suppose that:
- $G \cap \left({A \setminus \left\{{x}\right\}}\right) \ne \varnothing$.

- Then by definition of the empty set there exists $g$ such that:
- $g \in G \cap \left({A \setminus \left\{{x}\right\}}\right)$

- Hence by definition of intersection:
- $g \in G$ and
- $g \in A \setminus \left\{{x}\right\}$.

- Then by definition of set difference:
- $g \in A$

- Hence by definition of intersection:
- $g \in A \cap G$

- Then by $(3)$:
- $x = g$

- Hence this by definition of singleton contadicts with $g \notin \left\{{x}\right\}$ obtained by definition of set difference.
- Thus $G \cap \left({A \setminus \left\{{x}\right\}}\right) = \varnothing$.

Define $U = G \setminus \{x\}$ as an open set by $(4)$.

By $(5)$ and definition of set difference:

- $y \in A'$

Then by $(8)$ and Characterization of Derivative by Open Sets there exists a point $q$ of $T$ such that

- $(10): \quad q \in A \cap U$ and
- $(11): \quad y \ne q$.

By $(10)$ and definition of intersection:

- $q \in A$

By $(11)$ and definition of singleton:

- $q \notin \left\{{y}\right\}$

Then by definition of set difference

- $(12): \quad q \in A \setminus \left\{{y}\right\}$.

By definition of intersection:

- $q \in U$.

Then by $(12)$ and by definition of set difference

- $q \ne x$ and $q \in A$.

Then by definition of set difference:

- $q \in A \setminus \{x\}$

and

- $q \in G$.

Hence this contradicts with $(9)$ by definition of intersection.

Thus the result by Proof by Contradiction.

$\blacksquare$

## Sources

- Mizar article TOPGEN_1:32