avewright/proofwiki-math huggingface dataset:
Theorem: Non-Forking Types have Non-Forking Completions

Let $T$ be a complete $\LL$-theory.
Let $\mathfrak C$ be a monster model for $T$.
Let $A\subseteq B$ be subsets of the universe of $\mathfrak C$.
Let $\map \pi {\bar x}$ be an $n$-type over $B$.
If $\pi$ does not fork over $A$, then there is a complete $n$-type $p$ over $B$ such that $\pi \subseteq p$ and $p$ does not fork over $A$.

Proof:
Suppose $\pi$ does not fork over $A$.
We will use Zorn's Lemma to find a candidate for the needed complete type.
Consider the collection $\Pi$ of all non-forking sets $\pi'$ of $\LL$-formulas with parameters from $B$ such that $\pi'$ contains $\pi$.
Order $\Pi$ by subset inclusion.
Since a set forks iff a finite subset forks, the union over any chain is still a non-forking set, and hence is an upper bound for the chain.
Thus, by Zorn's Lemma, there is a maximal (with respect to subset inclusion) $p$ in $\Pi$.
{{AimForCont}} $p$ is not complete.
:By definition, for some $\map \phi {\bar x, \bar b}$, $p$ contains neither $\map \phi {\bar x, \bar b}$ nor $\neg \map \phi {\bar x, \bar b}$.
:Since $p$ is non-forking, by Formula and its Negation Cannot Both Cause Forking, at least one of $p \cup \map \phi {\bar x, \bar b}$ or $p \cup \neg \map \phi {\bar x, \bar b}$ is non-forking as well.
:Hence $p$ is not maximal in $\Pi$, contradicting the choice of $p$.
Thus $p$ is complete.
{{qed}}
{{AoC|Zorn's Lemma}}
Category:Model Theory for Predicate Logic
262jboi322etvrempv319q4v3euq63k
Theorem: Forking is Local

Let $T$ be a complete $\LL$-theory.
Let $\mathfrak C$ be a monster model for $T$.
Let $A\subseteq B$ be subsets of the universe of $\mathfrak C$.
Let $\map \pi {\bar x}$ be an $n$-type over $B$.
$\pi$ forks over $A$ {{iff}} a finite subset of $\pi$ forks over $A$.

Proof:
Suppose $\pi$ forks over $A$.
:By definition, $\pi$ implies a disjunction of formulas which each divide over $A$.
:Since proofs are finite, this means that there is a finite subset of $\pi$ which implies this disjunction, completing this direction of the proof.
Suppose a finite subset of $\pi$ forks over $A$.
:By definition, the finite subset implies a disjunction of formulas which each divide over $A$.
:But then $\pi$ clearly implies this disjunction as well, completing this direction of the proof.
{{qed}}
Category:Model Theory for Predicate Logic
bsj67sln7rrh4tvqytp4cz8sjralc39
Theorem: Subset of Finite Set is Finite

Let $X$ be a finite set.
If $Y$ is a subset of $X$, then $Y$ is also finite.

Proof:
From the definition, $X$ is finite {{iff}} $\exists n \in \N$ such that there exists a bijection:
:$f: X \leftrightarrow \N_n$
where $\N_n$ is the set of all elements of $\N$ less than $n$, that is:
:$\N_n = \set {0, 1, 2, \ldots, n - 1}$
The case in which $X$ is empty is trivial.
We begin proving the following particular case:
:''If $X$ is finite and $a \in X$, then $X \setminus \set a$ is also finite.''
From Bijection between Specific Elements there exists a bijection $f: \N_n \to X$, which satisfies $\map f n = a$.
Next we prove the general case by induction.
Theorem: Fortissimo Topology is Topology

Let $T = \struct {S, \tau_p}$ be a Fortissimo space.
Then $\tau_p$ is a topology on $T$.

Proof:
=== {{Open-set-axiom|3|nolink}} ===
We have that $p \in \relcomp S \O = S$ so $\O \in \tau_p$.
We have that $\relcomp S S = \O$, and Empty Set is Countable, so $S \in \tau_p$.
{{qed|lemma}}
Theorem: Fortissimo Space is Completely Normal

Let $T = \struct {S, \tau_p}$ be a Fortissimo space.
Then $T$ is a completely normal space.

Proof:
We have:
:Fortissimo Space is $T_1$
:Fortissimo Space is $T_5$
and so by definition $T$ is completely normal.
{{qed}}
Theorem: Fortissimo Space is T1

Let $T = \struct {S, \tau_p}$ be a Fortissimo space.
Then $T$ is a $T_1$ space.

Proof:
From Fortissimo Space is Excluded Point Space with Countable Complement Space, $T$ is an expansion of a countable complement space.
Then we have that a Countable Complement Space is $T_1$.
Then from $T_1$ Property is Preserved under Expansion, $T$ is a $T_1$ space.
{{qed}}
Theorem: Fortissimo Space is Excluded Point Space with Countable Complement Space

Let $T = \struct {S, \tau_p}$ be a Fortissimo space.
Then $\tau_p$ is the minimal topology that is generated by the excluded point topology and the countable complement topology.

Proof:
Let $T_1 = \struct {S, \tau_1}$ be the excluded point space on $S$ from $p$.
Let $T_2 = \struct {S, \tau_2}$ be the countable complement space on $S$.
By definition:
:$\tau_1 = \set {H \subseteq S: p \in \relcomp S H} \cup \set S$ 
:$\tau_2 = \leftset {H \subseteq S: \relcomp S H}$ is countable $\rightset{} \cup \set \O$
By definition of Fortissimo space, we have:
:$U \in \tau_1 \implies U \in \tau_p$
:$U \in \tau_2 \implies U \in \tau_p$
So $\tau_1 \cup \tau_2 \subseteq \tau_p$.
Similarly:
:$U \in \tau_p \implies U \in \tau_1 \lor U \in \tau_2$
and so $\tau_p \subseteq \tau_1 \cup \tau_2$.
So $\tau_p = \tau_1 \cup \tau_2$ and the result follows from Union is Smallest Superset.
{{qed}}
Theorem: Fortissimo Space is T5

Let $T = \struct {S, \tau_p}$ be a Fortissimo space on an infinite set $S$.
Then $T$ is a $T_5$ space.

Proof:
Let $A, B \in \tau_p$ such that $A$ and $B$ are separated.
If $p \notin A$ and $p \notin B$ then $A$ and $B$ are both open.
Otherwise $p$ must be in exactly one of them, because if $p$ were in both they could not be separated.
{{WLOG}}, suppose $p \in A$.
Then $p \notin B$ so $B$ is open.
Now suppose $B$ were not closed.
Then $B$ is uncountable by definition of Fortissimo space.
But every open set not containing $p$ is co-countable in $S$.
So $p$ would be in $B^-$, where $B^-$ is the closure of $B$.
But then {{hypothesis}} $p \in A$.
So $A \cap B^- \ne \O$ and so $A$ and $B$ are not separated.
So $B$ must be closed.
Therefore $\relcomp S B$ is an open set such that $A \subseteq \relcomp S B$, and the $T_5$ separation axiom is satisfied.
{{qed}}
Theorem: Fortissimo Space is Lindelöf

Let $T = \struct {S, \tau_p}$ be a Fortissimo space.
Then $T$ is a Lindelöf space.

Proof:
Let $\CC$ be an open cover of $T$.
Then $\exists U \in \CC$ such that $p \in U$ and so $\relcomp S U$ is countable.
So $U$, together with an open neighborhood of each of the elements of $\relcomp S U$, is a countable subcover of $\CC$.
Hence the result by definition of Lindelöf space.
{{qed}}
Theorem: Fortissimo Space is not Sigma-Compact

Let $T = \struct {S, \tau}$ be a Fortissimo space.
Then $T$ is not a $\sigma$-compact space.

Proof:
From Compact Sets in Fortissimo Space we have that the only compact sets in $T$ are finite.
A union of countably many finite sets can not be an uncountable set.
Hence the result by definition of $\sigma$-compact space.
{{qed}}
Theorem: Fortissimo Space is not Separable

Let $T = \struct {S, \tau_p}$ be a fortissimo space on an uncountable set $S$.
Then $T$ is not a separable space.

Proof:
Let $U$ be a countable subset of $S$.
By the definition of the fortissimo space, $U$ is closed.
From Closed Set Equals its Closure, $U^- = U \ne S$.
Thus, by definition, $U$ is not everywhere dense in $T$.
Thus, there exists no countable subset of $S$ which is everywhere dense in $T$.
So, by definition, $T$ is not a separable space.
{{qed}}
Theorem: Fortissimo Space is not First-Countable

Let $T = \struct {S, \tau_p}$ be a Fortissimo space.
Then $T$ is not a first-countable space.

Proof:
This proof follows the proof from Countable Complement Space is not First-Countable.
{{AimForCont}} that $p \in S$ has a countable local basis.
That means:
:there exists a countable set of sets $\BB_p \subseteq \tau$
such that:
:$\forall B \in \BB_p: p \in B$
and such that:
:every open neighborhood of $p$ contains some $B \in \BB_p$.
So:
{{begin-eqn}}
{{eqn | l = \bigcap \BB_p
      | r = \set p
      | c = 
}}
{{eqn | ll= \leadsto
      | l = S \setminus \set p
      | r = S \setminus \bigcap \BB_p
      | c = 
}}
{{eqn | r = \bigcup_{B \mathop \in \BB_p} \paren {S \setminus B}
      | c = De Morgan's Laws: Difference with Intersection
}}
{{end-eqn}}
By definition of the fortissimo space, each of $S \setminus B$ is countable.
From Countable Union of Countable Sets is Countable it follows that $\ds \bigcup_{B \mathop \in \BB_p} \paren {S \setminus B}$ is also countable.
So $S \setminus \set p$ and therefore $S$ is also countable.
From this contradiction (as we have specified that $S$ is uncountable), it follows that our assumption that $p \in S$ has a countable local basis must be false.
Hence by definition $T$ cannot be first-countable.
{{qed}}
Theorem: Modified Fort Topology is Topology

Let $T = \struct {S, \tau_{a, b} }$  be a modified Fort space.
Then $\tau_{a, b}$ is a topology on $S$.

Proof:
Let $S = N \cup \set {a, b}$ where $N$ is infinite, $a \ne b$ and $a, b \notin N$.
{{Recall|Modified Fort Space|modified Fort space}}
{{:Definition:Modified Fort Space}}
Theorem: Subset of Naturals is Finite iff Bounded

Let $X$ be a subset of the natural numbers $\N$.
Then $X$ is finite {{iff}} it is bounded.

Proof:
A subset of the natural numbers is also a subset of the real numbers $\R$.
By definition, a bounded subset of $\R$ is bounded below in $\R$ and bounded above in $\R$.
By the Well-Ordering Principle, $X$ is bounded below
Thus $X$ is bounded {{iff}} $X$ is bounded above.
That is, {{iff}}:
:$\exists p \in \N: \forall x \in X: x \le p$
Theorem: Arens-Fort Topology is Topology

Let $T = \struct {S, \tau}$ be the Arens-Fort space.
Then $\tau$ is a topology on $T$.

Proof:
=== {{Open-set-axiom|3|nolink}} ===
We have that $\tuple {0, 0} \notin \O$ so $\O \in \tau$.
We have that $\forall m: \set {n: \tuple {m, n} \notin S} = \O$ which is finite, so $S \in \tau$.
{{qed|lemma}}
Theorem: Arens-Fort Space is Expansion of Countable Fort Space

Let $T = \struct {S, \tau}$ be the Arens-Fort space, where $S = \Z_{\ge 0} \times \Z_{\ge 0}$.
Let $T_p = \struct {S, \tau_p}$ be the Fort space on $S$ where $p = \left({0, 0}\right)$.
Then $\tau$ is an expansion of $\tau_p$.
Furthermore, $S$ is countably infinite, so $T_p$ is a countable Fort space.

Proof:
Let $H \in \tau_p$ where $p = \tuple {0, 0}$.
Then either:
:$(1): \quad \tuple {0, 0} \in \relcomp S H$
or:
:$(2): \quad H$ is cofinite in $S$, that is $\relcomp S H$ is finite.
Case $(1)$ means that $\tuple {0, 0} \notin H$ and so $H \in \tau$ by definition of the Arens-Fort space.
Suppose case $(2)$ applies.
Then for all $m \in \Z_{\ge 0}$, the sets $S_m$ defined as $S_m = \set {n: \tuple {m, n} \notin H}$ are finite.
Thus in a finite number of these (that is, none of them) the set $S_m$ is infinite.
So $H \in \tau$.
So, if $H \in \tau_p$ it follows that $H \in \tau$ and so $\tau_p \subseteq \tau$.
Hence the result by definition of expansion.
Finally, from Arens-Fort Space is Countable we have that $S$ is countably infinite.
{{qed}}
Theorem: Arens-Fort Space is T1

Let $T = \struct {S, \tau}$ be the Arens-Fort space.
Then $T$ is a $T_1$ space.

Proof:
We have that the Arens-Fort Space is $T_2$.
The result follows from $T_2$ Space is $T_1$ Space.
{{qed}}
Theorem: Arens-Fort Space is T2.5

Let $T = \struct {S, \tau}$ be the Arens-Fort space.
Then $T$ is a $T_{2 \frac 1 2}$ space.

Proof:
We have:
:Fort Space is $T_{2 \frac 1 2}$
:Arens-Fort Space is Expansion of Fort Space.
The result follows from $T_{2 \frac 1 2}$ Property is Preserved under Expansion.
{{qed}}
Category:Arens-Fort Space
Category:Examples of T2.5 Spaces
63vekqpmf9f0cu6tne4djia88gxy7v1
Theorem: Arens-Fort Space is T5

Let $T = \struct {S, \tau}$ be the Arens-Fort space.
Then $T$ is a $T_5$ space.

Proof:
Let $A, B \subseteq S$ such that $A$ and $B$ are separated.
Let $p = \tuple {0, 0}$.
If $p \notin A$ and $p \notin B$ then $A$ and $B$ are both open and the problem is solved.
Otherwise $p$ must be in exactly one of them, because if $p$ were in both they could not be separated.
{{WLOG}}, suppose $p \in A$.
Then $p \notin B$ so $B$ is open.
$B \cup \set p$ is closed by the definition of the Arens-Fort space.
From Set is Subset of its Topological Closure and Set Closure is Smallest Closed Set in Topological Space:
:$B \subseteq B^- \subseteq B \cup \set p$
where $B^-$ is the closure of $B$.
So $B$ is closed or $p$ is in $B^-$.
But then {{hypothesis}} $p \in A$.
So $A \cap B^- \ne \O$ and so $A$ and $B$ are not separated.
So $B$ must be closed.
Therefore $\relcomp S B$ is an open set such that $A \subseteq \relcomp S B$, and the $T_5$ separation axiom is satisfied.
{{qed}}
Theorem: Arens-Fort Space is Completely Normal

Let $T = \struct {S, \tau}$ be the Arens-Fort space.
Then $T$ is a completely normal space.
Consequently, $T$ satisfies all weaker separation axioms.

Proof:
We have:
:Arens-Fort Space is $T_1$
:Arens-Fort Space is $T_5$
and so by definition $T$ is completely normal.
{{qed}}
See Sequence of Implications of Separation Axioms for confirmation of the statement about weaker separation axioms.
Theorem: Arens-Fort Space is not First-Countable

Let $T = \struct {S, \tau}$ be the Arens-Fort space.
Then $T$ is not a first-countable space.

Proof:
{{AimForCont}} $T$ is first-countable.
Then there exists a countable local base $\ds B_0 = \sequence {U_i}_{i \mathop = 1}^\infty$ for $\tuple {0, 0}$.
Suppose there does not exist a point $\tuple {n_i, m_i} \in U_i$ such that $n_i > i$ and $m_i > i$.
Then:
:$\forall \tuple {n, m} \in U_i: n \le i$ or $m \le i$
Now suppose that there does not exist some $\tuple {n, m} \in U_i$ with $n > i$.
Let $S_k$ be defined as:
:$S_k = \set {n: \tuple {k, n} \notin U_i}$
The definition of the Arens-Fort space clearly stipulates that $S_k$ can only be a infinite set for a finite number of $k \in \Z_{\ge 0}$.
But:
:$k > i \implies S_k = \Z_{\ge 0}$
So we have shown that:
:$\exists \tuple {n, m} \in U_i: n > i$
So, let $n > i$, and let $m \le i$.
Then $\set {m: m > i} \subseteq S_n$. 
Thus $S_n = \set {m: \tuple {n, m} \notin U_i}$ is infinite for all $n > i$.
Again, this contradicts the definition of the Arens-Fort space.
So, from the definition of the neighborhood of $\tuple {0, 0}$, for each $U_i \in B_0$ there is a point $\tuple {n_i, m_i} \in U_i$ such that both $n_i > i$ and $m_i > i$.
Now let the set $E$ be constructed as:
:$E := X \setminus \sequence {\tuple {n_i, m_i} }_{i \mathop = 1}^\infty$
We now prove that $E$ is a neighborhood of $\tuple {0, 0}$.
By the definition of Arens-Fort space, it is enough to show that:
:$\forall i \in \N: S_i$ is finite.
We have that:
{{begin-eqn}}
{{eqn | l = S_i
      | r = \set {m: \tuple {i, m} \notin E}
      | c = 
}}
{{eqn | r = \set {m: \tuple {i, m} \in \sequence {\tuple {n_j, m_j} }_{j \mathop = 1}^\infty}
      | c = 
}}
{{end-eqn}}
But we defined $n_j > j$.
So if $j > i \implies n_j > j > i$.
Thus $S_i \subseteq \sequence {m_j}_{j \mathop = 1}^i$ is finite. 
However, $\tuple {n_i, m_i} \notin E$.
Therefore there exists no $U_i \subseteq E$.
From this contradiction it follows that $T$ cannot be first-countable.
{{qed}}
{{proofread}}
Theorem: Countable Space is Separable

Let $T = \struct {S, \tau}$ be a topological space where $S$ is a countable set.
Then $T$ is a separable space.

Proof:
By definition, a topological space $T = \struct {S, \tau}$ is separable if there exists a countable subset of $S$ which is everywhere dense in $T$.
The closure of $S$ in $S$ is trivially $S$.
So, by definition, $S$ is everywhere dense in $S$.
As $S$ is countable by definition, the result follows.
{{qed}}
Category:Separable Spaces
Category:Countable Sets
5sagq1qbpwtck3uym0x314bh0a672vu
Theorem: Arens-Fort Space is Separable

Let $T = \struct {S, \tau}$ be the Arens-Fort space.
Then $T$ is a separable space.

Proof:
We have that the Arens-Fort space is an expansion of a countable Fort space.
So $S$ is countable.
The result follows from Countable Space is Separable.
{{qed}}
Theorem: Arens-Fort Space is Sigma-Compact

Let $T = \struct {S, \tau}$ be the Arens-Fort space.
Then $T$ is a $\sigma$-compact space.

Proof:
From Arens-Fort Space is Countable we have that $S$ is countably infinite.
Let $\tau_d$ be the discrete topology on $S$.
Consider the identity function $I_S: \struct {S, \tau_d} \to \struct {S, \tau}$.
From Mapping from Discrete Space is Continuous, $I_S$ is continuous.
From Identity Mapping is Surjection, $I_S$ is a surjection.
From:
:Countable Discrete Space is Sigma-Compact
:Sigma-Compactness is Preserved under Continuous Surjection
we conclude that $T$ is a $\sigma$-compact space.
{{qed}}
Theorem: Arens-Fort Space is Sigma-Compact

Let $T = \struct {S, \tau}$ be the Arens-Fort space.
Then $T$ is a $\sigma$-compact space.

Proof:
The result follows from:
:Arens-Fort Space is Countable
:Countable Space is $\sigma$-Compact.
{{qed}}
Theorem: Arens-Fort Space is Lindelöf

Let $T = \struct {S, \tau}$ be the Arens-Fort space.
Then $T$ is a Lindelöf space.

Proof:
We have:
:The Arens-Fort Space is $\sigma$-Compact.
:A $\sigma$-compact space is Lindelöf Space.
{{qed}}
Theorem: Arens-Fort Space is not Weakly Locally Compact

Let $T = \struct {S, \tau}$ be the Arens-Fort space.
Then $T$ is not a weakly locally compact space.

Proof:
We have that Neighborhood of Origin in Arens-Fort Space is not Compact.
So $\tuple {0, 0}$ is a point in $S$ which is not contained in a compact neighborhood.
Hence, by definition, $T$ is not weakly locally compact.
{{qed}}
Theorem: Arens-Fort Space is not Compact

Let $T = \struct {S, \tau}$ be the Arens-Fort space.
Then $T$ is not a compact space.

Proof:
Follows from:
:Arens-Fort Space is not Weakly Locally Compact
:Compact Space is Weakly Locally Compact.
{{qed}}
Theorem: Arens-Fort Space is not Countably Compact

Let $T = \struct {S, \tau}$ be the Arens-Fort space.
Then $T$ is not a countably compact space.

Proof:
{{AimForCont}} the Arens-Fort space is countably compact.
From Arens-Fort Space is Lindelöf, it is also Lindelöf.
From Countably Compact Lindelöf Space is Compact, $T$ is compact.
But this contradicts  Arens-Fort Space is not Compact.
Hence the result from Proof by Contradiction.
{{qed}}
Theorem: T3 Lindelöf Space is Paracompact

Let $T = \struct {S, \tau}$ be a $T_3$ space which is also Lindelöf.
Then $T$ is paracompact.

Proof:
Follows directly from:
{{begin-itemize}}
{{item||$T_3$ Lindelöf Space is Strongly Paracompact}}
{{item||Strongly Paracompact Space is Paracompact}}.
{{end-itemize}}
{{qed}}
Theorem: Arens-Fort Space is Paracompact

Let $T = \struct {S, \tau}$ be the Arens-Fort space.
Then $T$ is a paracompact space.

Proof:
Let $\CC$ be any open cover of $T$.
Let $H \in \CC$ be any open set which contains $\tuple {0, 0}$.
For all $s \in S$ such that $s \ne \tuple {0, 0}$, we have that $\set s$ is open in $T$ by definition of the Arens-Fort space.
So the open cover of $T$ which consists of $H$ together with all the open sets $\set s$, where $s \in S \setminus H$ is a refinement of $T$ which is locally finite.
Hence the result, by definition of paracompact space.
{{qed}}
Theorem: Arens-Fort Space is Paracompact

Let $T = \struct {S, \tau}$ be the Arens-Fort space.
Then $T$ is a paracompact space.

Proof:
We have that:
:Arens-Fort Space is Lindelöf
:Arens-Fort Space is $T_3$.
The result follows from $T_3$ Lindelöf Space is Paracompact.
{{qed}}
Theorem: First-Countability is not Continuous Invariant

Let $T_A = \struct {A, \tau_A}$ and $T_B = \struct {B, \tau_B}$ be topological spaces.
Let $\phi: T_A \to T_B$ be a continuous mapping.
If $T_A$ is a first-countable space, then it does not necessarily follow that $T_B$ is also first-countable.

Proof:
Let $T_S = \struct {S, \tau_S}$ be the Arens-Fort space.
Let $T_D = \struct {S, \tau_D}$ be the discrete space, also on $S$.
Let $I_S: S \to S$ be the identity mapping on $S$.
From Mapping from Discrete Space is Continuous, we have that $I_S$ is a continuous mapping.
Then we have:
:Discrete Space is First-Countable
:Arens-Fort Space is not First-Countable
Thus we have demonstrated a continuous mapping from a first-countable space to a space which is not first-countable space.
{{qed}}
Theorem: Second-Countability is not Continuous Invariant

Let $T_A = \struct {A, \tau_A}$ and $T_B = \struct {B, \tau_B}$ be topological spaces.
Let $\phi: T_A \to T_B$ be a continuous mapping.
If $T_A$ is a second-countable space, then it does not necessarily follow that $T_B$ is also second-countable.

Proof:
Let $T_S = \struct {S, \tau_S}$ be the Arens-Fort space.
Let $T_D = \struct {S, \tau_D}$ be the discrete space, also on $S$.
As $S$ is countable, from Arens-Fort Space is Expansion of Countable Fort Space, it follows that $T_D = \struct {S, \tau_D}$ is a countable discrete space.
Let $I_S: S \to S$ be the identity mapping on $S$.
From Mapping from Discrete Space is Continuous, we have that $I_S$ is a continuous mapping.
Then we have that a Countable Discrete Space is Second-Countable.
We have that the Arens-Fort Space is not First-Countable.
It follows from Second-Countable Space is First-Countable Space that the Arens-Fort space is not second-countable either.
Thus we have demonstrated a continuous mapping from a second-countable space to a space which is not second-countable.
{{qed}}
Theorem: Arens-Fort Space is not Connected

Let $T = \struct {S, \tau}$ be the Arens-Fort space.
Then $T$ is not a connected space.

Proof:
Consider $p \in S$ such that $p \ne \tuple {0, 0}$.
From Clopen Points in Arens-Fort Space, we have that $\set p$ is both open and closed in $T$.
So by definition of closed set, $\relcomp S {\set p}$ is also both open and closed in $T$.
So, by definition, $\set p \mid \relcomp S {\set p}$ is a separation of $T$
Hence the result, by definition of connected space.
{{qed}}
Theorem: Arens-Fort Space is not Locally Connected

Let $T = \struct {S, \tau}$ be the Arens-Fort space.
Then $T$ is not a locally connected space.

Proof:
Let $\UU_0$ be a local basis for $\tuple {0, 0}$.
Let $U \in \UU_0$.
By definition of local basis, $U$ is open in $T$.
From Clopen Points in Arens-Fort Space, $\set {\tuple {0, 0} }$ is not open in $T$.
So $U \ne \set {\tuple {0, 0} }$. 
Therefore:
:$\exists p \in U: p \ne \tuple {0, 0}$
From Singleton of Element is Subset:
:$\set p \subseteq U$
From Clopen Points in Arens-Fort Space it follows that $\set p$ is clopen.
As $U \in U_0$ it follows by definition of local basis that:
:$\tuple {0, 0} \in U$
and so:
:$U \ne \set p$
That is:
:$\set p \subsetneq U$
From Connected iff no Proper Clopen Sets, the set $U$ is not connected.
{{explain|Re-establish the definition of Definition:Connected Topological Space as the current flow does not make it obvious that a connected subset has no proper clopen sets, only that this condition applies to the full space.}}
It is deduced that any local basis is formed with disconnected sets.
Thus, by definition, $T$ is not locally connected.
{{qed}}
Theorem: Clopen Points in Arens-Fort Space

Let $T = \struct {S, \tau}$ be the Arens-Fort space.
Let $q \in S: q \ne \tuple {0, 0}$.
Then $\set q$ is both open and closed in $T$.
$\set {\tuple {0, 0} }$ itself is closed, but not open.

Proof:
We have that $\set q$ is finite so $\relcomp S {\set q}$ is cofinite.
So $\relcomp S {\set q}$ is open and so $\set q$ is closed.
Then we have that $\tuple {0, 0} \notin \set q$ so $\set q$ is open.
However, $\tuple {0, 0} \notin \relcomp S {\set {\tuple {0, 0} } }$ and $\relcomp S {\set {\tuple {0, 0} } }$ is clearly not open in $T$.
But as $\set {\tuple {0, 0} }$ is finite so $\relcomp S {\set {\tuple {0, 0} } }$ is cofinite.
Hence, as for $\set q$, we have that $\set {\tuple {0, 0} }$ is closed.
{{qed}}
Theorem: Neighborhood of Origin of Arens-Fort Space is Closed

Let $T = \struct {S, \tau}$ be the Arens-Fort space.
Every neighborhood of $\tuple {0, 0}$ is closed in $T$.

Proof:
Let $H \subseteq S$ such that:
:$\exists U \in \tau: \tuple {0, 0} \in U \subseteq H \subseteq S$
that is: such that $H$ is a neighborhood of $\tuple {0, 0}$ in $T$.
As $\tuple {0, 0} \in H$ it follows that $\tuple {0, 0} \notin \relcomp S H$.
So, by definition of the Arens-Fort space, $\relcomp S H$ is open in $T$.
So by definition, we have that $H$ is closed.
{{qed}}