avewright/proofwiki-math huggingface dataset:
Theorem: Compactness Theorem

Let $\LL$ be the language of predicate logic.
Let $T$ be a set of $\LL$-sentences.
Then $T$ is satisfiable {{iff}} $T$ is finitely satisfiable.

Proof:
By Extend Theory to Satisfy Witness Property, there exist a language $\LL^*$ and a set of $\LL^*$-sentences $T^*$ satisfying:
* $T^*$ is finitely satisfiable
* If $T^*$ is satisfiable, then $T$ is satisfiable
* For every $\LL^*$-WFF of $1$ free variable $\map \phi x$, there exists some constant $c_\phi$ such that:
::$T^* \models \paren {\exists x: \map \phi x} \implies \map \phi {x := c_\phi}$
Thus, it suffices to show that $T^*$ is satisfiable.
By Finitely Satisfiable Set of Sentences has Maximal Finitely Satisfiable Extension, there exists a set of $\LL^*$-sentences $T' \supseteq T^*$ such that:
:For all $\LL^*$-sentences $\phi$, either $\phi \in T'$ or $\sqbrk {\neg \phi} \in T'$
As $T^* \subseteq T'$, it follows that the third property above continues to hold for $T'$.
Thus, by the lemma to Extend Theory to Satisfy Witness Property:
:$T'$ satisfies the witness property
Additionally, any $\mathrm{PL}$-structure that models $T'$ will also model $T^*$.
But, by Maximal Finitely Satisfiable Theory with Witness Property is Satisfiable, there is such a $\mathrm{PL}$-structure.
{{qed}}
Theorem: Compactness Theorem

Let $\LL$ be the language of predicate logic.
Let $T$ be a set of $\LL$-sentences.
Then $T$ is satisfiable {{iff}} $T$ is finitely satisfiable.

Proof:
This proof is by contraposition.
The idea is to exploit the finiteness of proofs and the relation between satisfiability and deducibility to show that if $T$ is not satisfiable, then it must have a finite subset which can be used to prove to a contradiction.
Suppose $T$ is not satisfiable.
Since $T$ has no models, it vacuously follows that $T \models \phi \wedge \neg \phi$ for some sentence $\phi$.
By Gödel's Completeness Theorem, this implies that $\phi \wedge \neg \phi$ is deducible from $T$.
But any deduction from $T$ involves only finitely many sentences from $T$.
This means that there is a finite subset $\Delta$ of $T$ such that $\phi \wedge \neg \phi$ is deducible from $\Delta$.
By Soundness of First-Order Logic, this means that $\Delta \models \phi \wedge \neg \phi$.
Thus $\Delta$ is not satisfiable.
By the Rule of Transposition, $\Delta$ is satisfiable implies $T$ is satisfiable.
{{qed}}
Theorem: Compactness Theorem

Let $\LL$ be the language of predicate logic.
Let $T$ be a set of $\LL$-sentences.
Then $T$ is satisfiable {{iff}} $T$ is finitely satisfiable.

Proof:
This proof actually demonstrates a stronger form of the Compactness Theorem by showing:
:If $T$ is finitely satisfiable and $\kappa$ is an infinite cardinal such that $\kappa > \size \LL$, then $T$ is satisfiable by a model whose cardinality is at most $\kappa$.
This is stronger than the original statement, since it provides extra information about the model that is claimed to exist.
The proof is said to use a Henkin Construction because it involves the construction of a model all of whose elements are interpretations of the constant symbols of some language.
Such a model was used in {{AuthorRef|Leon Albert Henkin}}'s proof of the Completeness Theorem.
This special feature of the constructed model is what allows us to control its cardinality.
First, by Extend Theory to Satisfy Witness Property, we can extend $\LL$ and $T$ to find a language $\LL^*$ of cardinality at most $\kappa$ and an $\LL^*$-theory $T^*$ such that all finitely satisfiable $\LL^*$-theories containing $T^*$ have the witness property.
Then, since finitely satisfiable theories have maximal finitely satisfiable extensions, we can find a finitely satisfiable $\LL^*$-theory $T'$ containing $T^*$ such that $T'$ contains either $\phi$ or $\neg\phi$ for each $\LL^*$-sentence $\phi$.
Note that $T'$ has the witness property since it contains $T^*$.
Finally, by Maximal Finitely Satisfiable Theory with Witness Property is Satisfiable, $T'$ has a model.
Moreover, since $\LL^*$ has cardinality at most $\kappa$ and hence has at most $\kappa$-many constant symbols, this theorem ensures that the model of $T'$ can be taken to have cardinality at most $\kappa$.
{{qed}}
Theorem: Compactness Theorem

Let $\LL$ be the language of predicate logic.
Let $T$ be a set of $\LL$-sentences.
Then $T$ is satisfiable {{iff}} $T$ is finitely satisfiable.

Proof:
The idea is to construct an ultraproduct using a purposefully selected ultrafilter and collection of models so that each sentence in $T$ will be realized as a result of Łoś's Theorem.
Let $\Sigma$ be the set of all finite subsets of $T$.
For every $\Sigma_0 \in \Sigma$, define:
:$F_{\Sigma_0} = \set {\Delta \in \Sigma: \Sigma_0 \subseteq \Delta}$
That is, $F_{\Sigma_0}$ is the collection of all finite subsets of $T$ including $\Sigma_0$.
Clearly $F_{\Sigma_0}$ is a subset of $\Sigma$.
Now define:
:$F = \set {F_{\Sigma_0}: \Sigma_0 \in \Sigma}$
a subset of $\powerset \Sigma$.
We claim this has the finite intersection property.
Take any finite collection $\ds \set {F_{\Sigma_k} }_{k = 1, 2, \dots, n}$ of elements on $F$, and observe that the set $\ds S = \bigcup_{k \mathop = 1}^n \Sigma_k$ is a finite subset of $T$.
That is, $S \in \Sigma$.
$S \in F_{\Sigma_k}$ for each $k$ by construction, and hence is in their intersection.
In fact, their intersection is $F_S$.
So the intersection of any finite collection of elements of $F$ is nonempty as claimed.
Since $F$, which is a set of subsets of $\Sigma$, has the finite intersection property, there is an ultrafilter $U$ on $\Sigma$ including it (by {{Corollary|Ultrafilter Lemma}}). 
If $\Sigma_0 \in \Sigma$, then by assumption it has a model $\AA_{\Sigma_0}$.
Define:
:$\ds \AA = \paren {\prod_{\Sigma_k \mathop \in \Sigma} \AA_{\Sigma_k} } / U$
We verify $\AA \models T$.
Take any $\phi \in T$.
Observe that $F_{\set \phi} \in U$ by definition of $U$.
Furthermore, if we define $\Phi = \set {\Sigma_0 \in \Sigma: \AA_{\Sigma_0} \models \phi}$, we have $F_{\set \phi} \subseteq \Phi$.
Hence, since $U$ is a filter and $F_{\set \phi} \in U$, $\Phi \in U$.
Then Łoś's Theorem implies that $\AA \models \phi$.
{{qed}}
Theorem: Closed Extension Topology is Topology

Let $T = \struct {S, \tau}$ be a topological space.
Let $\tau^*_p$ be the closed extension topology of $\tau$.
Then $\tau^*_p$ is a topology on $S^*_p = S \cup \set p$.

Proof:
By definition:
:$\tau^*_p = \set {U \cup \set p: U \in \tau} \cup \set \O$
We have that $\O \in \tau^*_p$ by definition.
We also have that $S \in \tau$ so $S \cup \set p \in \tau^*_p$.
Now let $U_1, U_2 \in \tau^*_p$.
Then $U_1^* = U_1 \setminus \set p \in \tau, U_2^* = U_2 \setminus \set p \in \tau$.
Then $p \in U_1$ and $p \in U_2$ and so $p \in U_1 \cap U_2$.
So $U_1 \cap U_2 = \paren {U_1^* \cap U_2^*} \cup \set p \in \tau^*_p$. 
Finally consider $\UU \subseteq \tau^*_p$.
:$\ds \bigcup \UU = \bigcup_{U \mathop \in \UU} \paren {U \setminus \set p} \cup \set p$
So $\ds \bigcup \UU \in \tau^*_p$.
So $\tau^*_p$ is a topology on $S \cup \set p$.
{{qed}}
Theorem: Tarski-Vaught Test

Let $\MM, \NN$ be $\LL$-structures such that $\MM$ is a substructure of $\NN$.
{{wtd|The page Definition:Structure is a disambiguation page, in which the form in which it is used here may not be included. The level of clarity in this page generally needs improving. Hence the invocation of the Disambiguate template.}}
{{Disambiguate|Definition:Structure}}
Then $\MM$ is an elementary substructure of $\NN$ {{iff}}:
:for every $\LL$-formula $\map \phi {x, \bar v}$ and for every $\bar a$ in $\MM$:
::if there exists an $n$ in $\nN$ such that $\NN \models \map \phi {n, \bar a}$
::then there exists an $m$ in $\MM$ such that $\NN \models \map \phi {m, \bar a}$.
{{wtd|Before sense can be made of this page, Definition:Substructure and  Definition:Elementary Substructure need to be written.}}
{{Disambiguate|Definition:Logical Formula}}
The condition on the right side of the {{iff}} statement above can be rephrased as:
:Every existential statement with parameters from $\MM$ which is satisfied in $\NN$ can be witnessed by an element from the substructure $\MM$.

Proof:
=== Sufficient Condition ===
Let $\MM$ be an elementary substructure of $\NN$.
Then $\NN \models \exists x: \map \phi {x, \bar a}$ implies that $\MM \models \exists x: \map \phi {x, \bar a}$.
Hence there exists some $m$ in $\MM$ such that:
:$\MM \models \map \phi {m, \bar a}$.
Passing back up to $\NN$ yields the result.
{{explain|Worth making it explicit exactly what that result is, so as to clarify what is being sought here.}}
{{qed|lemma}}
Theorem: Quantifier Free Formula is Preserved by Superstructure

Let $\MM, \NN$ be $\LL$-structures such that  $\MM$ is a substructure of $\NN$.
Let $\map \phi {\bar x}$ be a quantifier-free $\LL$-formula, and let $\bar a \in\MM$.
Then $\MM \models \map \phi {\bar a}$ {{iff}} $\NN \models \map \phi {\bar a}$.

Proof:
The proof is done by induction on complexity of formulas.
Note that since interpretations of terms with parameters from $\MM$ are preserved when passing to superstructures, we have that $\map {t^\MM} {\bar a} = \map {t^\NN} {\bar a}$ whenever $t$ is an $\LL$-term and $\bar a$ is in $\MM$.
First, we verify the theorem for atomic formulas.  This is the base for the inductive proof.
Suppose $\phi$ is $t_1 = t_2$ for terms $t_1$ and $t_2$:
We have $\MM \models \map \phi {\bar a}$ {{iff}} $\MM \models \map {t_1} {\bar a} = \map {t_2} {\bar a}$.
The {{RHS}} of this holds {{iff}} $\map {t_1^\MM} {\bar a} = \map {t_2^\MM} {\bar a}$.
By the note above, this in turn holds {{iff}} $\map {t_1^\NN} {\bar a} = \map {t_2^\NN} {\bar a}$, which is equivalent to $\NN \models \map \phi {\bar a}$.
Suppose $\phi$ is $R(t_1, \dots, t_n)$ where $R$ is a relation symbol and each $t_i$ is a term:
We have:
:$\MM \models \map \phi {\bar a}$ iff $\paren {\map {t_1^\NN} {\bar a}, \dots, \map {t_n^\NN} {\bar a} } \in R^\MM$
Since $\MM$ is a substructure of $\NN$, the interpretation of $R$ in $\NN$ must extend $R^\MM$, so the right side of this statement is equiavlent to:
:$\paren {\map {t_1^\NN} {\bar a}, \dots, \map {t_n^\NN} {\bar a} } \in R^\NN$
By the note above, this in turn is equivalent to:
:$\paren {\map {t_1^\NN} {\bar a}, \dots, \map {t_n^\NN} {\bar a} } \in R^\NN$
which is the same as:
:$\NN \models \map \phi {\bar a}$
Having verified the theorem for the atomic formulas, we proceed with the inductive step of the proof.
Suppose the result holds for $\psi$, and consider $\neg \psi$:
We have $\MM \models \neg \map \psi {\bar a}$ {{iff}} $\MM \not \models \map \psi {\bar a}$.
By the inductive hypothesis, the right side of this statement is equivalent to $\NN \not\models \map \psi {\bar a}$, and so the result follows.
Suppose the result holds for $\psi_1$ and $\psi_2$.#
Consider $\psi_1 \wedge \psi_2$:
We have $\MM \models \map {\psi_1} {\bar a} \wedge \map {\psi_2} {\bar a}$ {{iff}} $\MM \models \map {\psi_1} {\bar a}$ and $\MM \models \map {\psi_2} {\bar a}$.
By the inductive hypothesis, the {{RHS}} of this is equivalent to $\NN \models \map {\psi_1} {\bar a}$ and $\NN \models \map {\psi_2} {\bar a}$.
The result follows, completing the proof.
{{qed}}
{{MissingLinks}}
Category:Model Theory for Predicate Logic
4wcazuhppkx76ny5tk73f1etvzueny6
Theorem: Algebraically Closed Field is Infinite

Let $F$ be an algebraically closed field.
Then $F$ is infinite.

Proof:
We prove the contrapositive: that a Galois field cannot be algebraically closed.
Let $F$ be Galois.
Define the polynomial:
:$\ds \map f x = 1 + \prod_{a \mathop \in F} \paren {x - a}$
By definition, a field is a ring.
Thus by Ring Product with Zero:
:$\ds \forall x \in F: \prod_{a \mathop \in F} \paren {x - a} = 0$
But:
:$\forall a \in F: \map f a = 1 + 0 \ne 0$
Therefore $\map f x$ cannot have a root in $F$.
Thus $F$ is not algebraically closed.
The result follows by the Rule of Transposition.
{{qed}}
Category:Field Theory
g39pp8ecmuzeh1hpou5i9k5611wyifr
Theorem: Theory of Algebraically Closed Fields of Characteristic p is Complete

Let $p$ be either $0$ or a prime number.
Let $ACF_p$ be the theory of algebraically closed fields of characteristic $p$ in the language $\LL_r = \set {0, 1, +, -, \cdot}$ for rings, where:
:$0, 1$ are constants
and:
:$+, -, \cdot$ are binary functions. 
Then $ACF_p$ is complete.

Proof:
By the Łoś-Vaught Test, it suffices to show that $ACF_p$ is satisfiable, has no finite models, and is $\kappa$-categorical for some uncountable $\kappa$.
Theorem: Lefschetz Principle (First-Order)

Let $\phi$ be a sentence in the language $\LL_r = \set {0, 1, +, -, \cdot}$ for rings, where $0, 1$ are constants and $+, -, \cdot$ are binary functions.
{{TFAE}}
:$(1): \quad \phi$ is true in every algebraically closed field of characteristic $0$.
:$(2): \quad \phi$ is true in some algebraically closed field of characteristic $0$.
:$(3): \quad \phi$ is true in algebraically closed fields of characteristic $p$ for arbitrarily large primes $p$.
:$(4): \quad \phi$ is true in algebraically closed fields of characteristic $p$ for sufficiently large primes $p$.
Note in particular that since $\C$ is an algebraically closed field of characteristic $0$, these are equivalent to $\phi$ being true in the field $\C$.

Proof:
=== $(1)$ iff $(2)$ ===
From Theory of Algebraically Closed Fields of Characteristic $p$ is Complete:
the theory $ACF_p$ of algebraically closed fields of characteristic $p$ is complete.
That is, all such fields satisfy the exact same $\LL_r$ sentences.
{{qed|lemma}}
Theorem: CNF Satisfiability Problem is NP-Complete

The conjunctive normal form boolean satisfiability problem (CNF SAT) is NP-complete.

Proof:
Let $P$ be a CNF SAT problem.
Theorem: Closed Sets of Closed Extension Topology

Let $T = \struct {S, \tau}$ be a topological space.
Let $T^*_p = \struct {S^*_p, \tau^*_p}$ be the closed extension space of $T$.
Then the closed sets of $T^*_p$ (apart from $S^*_p$) are the closed sets of $T$.
This explains why $\tau^*_p$ is called the closed extension topology of $\tau$.

Proof:
By definition:
:$\tau^*_p = \set {U \cup \set p: U \in \tau} \cup \set \O$
Let $V \subseteq S^*_p$ be closed in $T^*_p$.
Then $S^*_p \setminus V$ is open in $T^*_p$.
Then $\struct {S^*_p \setminus V} \setminus \set p$ is open in $T$.
From Set Difference with Union we have:
:$\struct {S^*_p \setminus V} \setminus \set p = S^*_p \setminus \struct {V \cup \set p}$
Hence the result.
{{qed}}
Theorem: Particular Point Topology is Closed Extension Topology of Discrete Topology

Let $S$ be a set and let $p \in S$.
Let $\tau_p$ be the particular point topology on $S$.
Let $T = \struct {S \setminus \set p, \vartheta}$ be the discrete topological space on $S \setminus \set p$.
Then $T^* = \struct {S, \tau_p}$ is a closed extension space of $T$.

Proof:
Directly apparent from the definitions of particular point topology, discrete topological space and closed extension space.
{{qed}}
Theorem: Closed Extension Topology is not T1

Let $T = \struct {S, \tau}$ be a topological space.
Let $T^*_p = \struct {S^*_p, \tau^*_p}$ be the closed extension space of $T$.
Then $T^*_p$ is not a $T_1$ space.

Proof:
By definition:
:$\tau^*_p = \set {U \cup \set p: U \in \tau} \cup \set \O$
Let $x \in S^*_p, x \ne p$.
Let $U = \set p$.
Then $U \in \tau^*_p$ such that $p \in U, x \notin U$.
But there is no $V \in \tau^*_p$ such that $x \in V, p \notin V$, by definition of the closed extension topology.
Hence $T^*_p$ can not be a $T_1$ space.
{{qed}}
Theorem: Algebraic Numbers are Countable

The set $\Bbb A$ of algebraic numbers is countable.

Proof:
By definition, $\Bbb A$ is the subset of the complex numbers which consists of roots of polynomials with coefficients in $\Q$.
We can prove the theorem by a cardinality argument, counting the number of such polynomials and roots.
By Set of Polynomials over Infinite Set has Same Cardinality, the set $\Q \sqbrk x$ of polynomials over $\Q$ is countable.
Next, note that $\Bbb A$ can be written as the union of the set of roots of each polynomial.
That is:
:$\Bbb A = \ds \bigcup_{\map p x \mathop \in \Q \sqbrk x} \set {x \in \C: \map p x = 0}$
From Polynomial over Field has Finitely Many Roots, $\Bbb A$ is a union of countably many finite sets.
From Countable Union of Countable Sets is Countable it follows that $\Bbb A$ is countable.
{{qed}}
Theorem: Limit Points in Closed Extension Space

Let $T = \struct {S, \tau}$ be a topological space.
Let $T^*_p = \struct {S^*_p, \tau^*_p}$ be the closed extension space of $T$.
Let $x \in S$.
Then $x$ is a limit point of $p$.

Proof:
Every open set of $T^*_p = \struct {S^*_p, \tau^*_p}$ except $\O$ contains the point $p$ by definition.
So every open set $U \in \tau^*_p$ such that $x \in U$ contains $p$.
So by definition of the limit point of a point, $x$ is a limit point of $p$.
{{qed}}
Theorem: Closure of Open Set of Closed Extension Space

Let $T = \struct {S, \tau}$ be a topological space.
Let $T^*_p = \struct {S^*_p, \tau^*_p}$ be the closed extension space of $T$.
Then:
:$U^- = S^*_p$
where $U^-$ denotes the closure of $U$ in $T^*_p$.

Proof:
By definition, $\forall U \in \tau^*_p, u \ne \O: p \in U$.
From Limit Points in Closed Extension Space, every point in $S^*_p$ is a limit point of $p$.
So by definition of closure, every point in $S^*_p$ is in $U^-$.
{{qed}}
Theorem: Closed Extension Space is Irreducible

Let $T = \struct {S, \tau}$ be a topological space.
Let $T^*_p = \struct {S^*_p, \tau^*_p}$ be the closed extension space of $T$.
Then $T^*_p$ is irreducible.

Proof:
Trivially, by definition, every open set in $T^*_p$ contains $p$.
So:
:$\forall U_1, U_2 \in \tau^*_p: p \in U_1 \cap U_2$
for $U_1, U_2 \ne \O$.
{{qed}}
Theorem: Closed Extension Space is Irreducible

Let $T = \struct {S, \tau}$ be a topological space.
Let $T^*_p = \struct {S^*_p, \tau^*_p}$ be the closed extension space of $T$.
Then $T^*_p$ is irreducible.

Proof:
From Closure of Open Set of Closed Extension Space we have that:
:$\forall U \in \tau^*_p: U \ne \O \implies U^- = S$
where $U^-$ is the closure of $U$.
The result then follows by definition of irreducible space.
{{qed}}
Theorem: Polynomial over Field has Finitely Many Roots

Let $F$ be a field.
Let $F \left[{x}\right]$ be the ring of polynomial functions in the indeterminate $x$.
If $p \in F \left[{x}\right]$ be non-null, then $p$ has finitely many roots in $F$.

Proof:
Let $n \ge 1$ be the degree of $p$.
We argue that $p$ has at most $n$ roots in $F$.
Let $A$ be the set of roots of $p$.
Let $a \in A$.
By the Polynomial Factor Theorem:
:$p \left({x}\right) = q_1 \left({x}\right) \cdot \left({x - a}\right)$
:where $\deg q_1 = n - 1$.
Let $a' \in A$ such that $a' \ne a$.
Then since:
:$p \left({a'}\right) = 0$
but:
:$\left({a' - a}\right) \ne 0$
it follows that:
:$q_1 \left({a'}\right) = 0$
Again by the Polynomial Factor Theorem:
:$q_1 \left({x}\right) = q_2 \left({x}\right) \cdot \left({x - a'}\right)$
Therefore:
:$p \left({x}\right) = q_2 \left({x}\right) \cdot \left({x - a'}\right) \cdot \left({x - a}\right)$
where $\deg q_2 = n-2$.
We can repeat this procedure as long as there are still distinct roots in $A$.
After the $i$th iteration we obtain a polynomial $q_i$ of degree $n-i$.
Now the degree of $q_i$ decreases each time we factor out a root of $p$, so $q_n$ is necessarily a constant term.
Therefore $q_n$ can share no roots with $p$.
So this procedure must stop by at most the $n$th step.
That is, we can pick at most $n$ distinct elements from the set $A$, and:
:$\left\vert{A}\right\vert \le n$
{{qed}}
Category:Polynomial Theory
6s0xud8pptm377rznzyfrdvezyq5w0x
Theorem: Set of Polynomials over Infinite Set has Same Cardinality

Let $S$ be a set of infinite cardinality $\kappa$.
Let $S \sqbrk x$ be the set of polynomial forms over $S$ in the indeterminate $x$.
Then $S \sqbrk x$ has cardinality $\kappa$.

Proof:
Since $S \sqbrk x$ contains a copy of $S$ as constant polynomials, we have an injection $S \to S \sqbrk x$.
We define an injection from $S \sqbrk x$ to the set $\FF$ of finite sequences over $S$ as follows:
Each polynomial in $f \in S \sqbrk x$ is of the form:
:$f = a_0 + a_1 x + a_2 x^2 + \dotsb + a_n x^n$
where $a_n$ is non-zero and each $a_i$ is in $S$.
We send each polynomial $f$ to the sequence of its coefficients $\sequence {a_0, \dotsc, a_n}$.
By the definition of equality of polynomials, this is injective.
Now the set of finite sequences over $S$ is a countable union of sets of cardinality $\kappa$.
From Cardinality of Infinite Union of Infinite Sets, $\FF$ has cardinality $\kappa$.
Therefore there is a bijection $\FF \leftrightarrow S$.
Composing this with the injection $S \sqbrk x \to \FF$, we have an injection $S \sqbrk x \to S$.
So by the Cantor-Bernstein-Schröder Theorem there is a bijection $S \sqbrk x \leftrightarrow S$.
Hence, we have:
:$\card {S \sqbrk x} = \card S = \kappa$
{{qed}}
Category:Polynomial Theory
3i9jas2873znq5vkcgjoszbtzmyvo25
Theorem: Excluded Point Topology is Topology

Let $T = \struct {S, \tau_{\bar p} }$ be an excluded point space.
Then $\tau_{\bar p}$ is a topology on $S$, and $T$ is a topological space.

Proof:
We have by definition that $S \in \tau_{\bar p}$, and as $p \notin \O$ we have that $\O \in \tau_{\bar p}$.
Now let $U_1, U_2 \in \tau_{\bar p}$.
By definition $p \notin U_1$ and $p \notin U_2$.
By definition of set intersection:
:$p \notin U_1 \cap U_2$
So $U_1 \cap U_2 \in \tau_{\bar p}$.
Now let $\UU \subseteq \tau_{\bar p}$.
We have that $\forall U \in \UU: p \notin U$.
Hence from Subset of Union $p \notin \bigcup \UU$.
So all the properties are fulfilled for $\tau_{\bar p}$ to be a topology on $S$.
{{qed}}
Theorem: Open Extension Topology is Topology

Let $T = \struct {S, \tau}$ be a topological space.
Let $\tau^*_{\bar p}$ be the open extension topology of $\tau$.
Then $\tau^*_{\bar p}$ is a topology on $S^*_p = S \cup \set p$.

Proof:
By definition:
:$\tau^*_{\bar p} = \set {U: U \in \tau} \cup \set {S^*_p}$
We have that $S^*_p \in \tau^*_{\bar p}$ by definition.
We also have that $\O \in \tau$ so $\O \in \tau^*_{\bar p}$.
Now let $U_1, U_2 \in \tau^*_{\bar p}$.
Then:
{{begin-eqn}}
{{eqn | l = U_1, U_2
      | o = \in
      | r = \tau
      | c = 
}}
{{eqn | ll= \leadsto
      | l = U_1 \cap U_2
      | o = \in
      | r = \tau
      | c = 
}}
{{eqn | ll= \leadsto
      | l = U_1 \cap U_2
      | o = \in
      | r = \tau^*_{\bar p}
      | c = 
}}
{{end-eqn}}
Finally consider $\UU \subseteq \tau^*_{\bar p}$.
Assuming $S^*_p \notin \UU$ we have that $\UU \subseteq \tau$.
So:
:$\ds\bigcup \UU \in \tau$
and so:
:$\ds \bigcup \UU \in \tau^*_p$
If $S^*_p \in \UU$ then:
:$\ds \bigcup \UU = S^*_p \in \tau^*_p$
So $\tau^*_p$ is a topology on $S \cup \set p$.
{{qed}}
Theorem: Excluded Point Topology is Open Extension Topology of Discrete Topology

Let $S$ be a set.
Let $p \in S$.
Let $\tau_{\bar p}$ be the excluded point topology on $S$.
Let $T = \struct {S \setminus \set p, \tau_D}$ be the discrete topological space on $S \setminus \set p$.
Then $T^* = \struct {S, \tau_{\bar p} }$ is an open extension space of $T$.

Proof:
Directly apparent from the definitions of excluded point topology, discrete topological space and open extension space.
{{qed}}
Theorem: Product of Countable Discrete Space with Sierpiński Space is Paracompact

Let $T_X = \struct {S, \tau}$ be a countable discrete space.
Let $T_Y = \struct {\set {0, 1}, \tau_0}$ be a Sierpiński space.
Let $T_X \times T_Y$ be the product space of $T_X$ and $T_Y$.
Then $T_X \times T_Y$ is paracompact.

Proof:
From Discrete Space is Paracompact, $T_X$ is paracompact.
We have that the Sierpiński space $T_Y$ is a finite topological space.
From Finite Topological Space is Compact, $T_Y$ is a compact space.
{{finish|Steen and Seebach in Part $\text I$ chapter $3$ Compactness: Invariance Properties offer "If $X$ is compact, then in general $X \times Y$ has the compactness properties of $Y$." Whether this holds for $Y$ paracompact needs to be investigated.}}