avewright/proofwiki-math huggingface dataset:
Theorem: Huygens-Steiner Theorem

Let $B$ be a body of mass $M$.
Let $I_0$ be the moment of inertia of $B$ about some axis $A$ through the centre of mass of $B$.
Let $I$ be the moment of inertia of $B$ about another axis $A'$ parallel to $A$.
Then $I_0$ and $I$ are related by:
:$I = I_0 + M l^2$
where $l$ is the distance between $A$ and $A'$.

Proof:
{{WLOG}}, suppose $I$ is oriented along the $z$-axis.
By definition of moment of inertia:
:$\ds I = \sum m_j \lambda_j^2$
:$\ds I_0 = \sum m_j \lambda_j'^2$
where:
:$\lambda_j$ is the position vector to the $j$th particle from the $z$-axis
:$\lambda_j'$ is related to $\lambda_j$ by:
::$\lambda_j = \lambda_j' + R_\perp$
:$R_\perp$ is the perpendicular distance from $A$ to the center of mass of $B$.
{{Proofread|Check that definition of $R_\perp$ -- distance of $B$ from $A$ or $A'$?}}
Therefore:
:$\ds I = \sum m_j \lambda_j^2 = \sum m_j \paren {\lambda_j'^2 + 2 \lambda_j' \cdot R_\perp + R_\perp^2}$
The middle term is:
:$\ds 2 R_\perp \cdot \sum m_j \lambda_j' = 2 R_\perp \cdot \sum m_j \paren {\lambda_j - R_\perp} = 2 R_\perp \cdot M \paren {R_\perp - R_\perp} = 0$
Thus:
:$\ds I = \sum m_j \lambda_j^2 = \sum m_j \paren {\lambda_j'^2 + R_\perp^2} = I_0 + M l^2$
{{Qed}}
Theorem: Equivalence of Definitions of Well-Ordering/Definition 1 implies Definition 2

Let $\struct {S, \preceq}$ be an ordered set such that:
:$\forall T \subseteq S: \exists a \in T: \forall x \in T: a \preceq x$
That is, such that $\preceq$ is a well-ordering by definition 1.
Then $\preceq$ is a total ordering.

Proof:
Consider $X = \set {a, b}$ where $a, b \in S$.
We have {{hypothesis}} that $X$ has a smallest element.
So either $\min X = a$ or $\min X = b$.
If $\min X = a$, then $a \preceq b$.
If $\min X = b$, then $b \preceq a$.
So either $a \preceq b$ or $b \preceq a$.
That is, $a$ and $b$ are comparable.
As this applies to all $a, b \in S$, the ordering $\preceq$ is total.
Theorem: Choice Function Exists for Well-Orderable Union of Sets

Let $\mathbb S$ be a set of sets such that:
:$\forall S \in \mathbb S: S \ne \O$
that is, none of the sets in $\mathbb S$ may be empty.
Let the union $\bigcup \mathbb S$ be well-orderable.
Then there exists a choice function $f: \mathbb S \to \bigcup \mathbb S$ defined as:
:$\forall S \in \mathbb S: \exists x \in S: \map f S = x$

Proof:
Suppose $T = \bigcup \mathbb S$ is well-orderable.
Then we can create a well-ordering $\preceq$ on $T$ so as to make $\struct {T, \preceq}$ a well-ordered set.
From the definition of well-ordered set, every subset of $T$ is itself well-ordered.
From Set is Subset of Union we have that:
:$\forall S \in \mathbb S: S \subseteq T$
So every $S \in \mathbb S$ is well-ordered and Choice Function Exists for Set of Well-Ordered Sets applies.
Indeed, if every element of $\mathbb S$ is well-ordered, then we can create a choice function $f$ defined as:
:$\forall S \in \mathbb S: \map f S = \inf S$
It may be the case that we are making infinitely many choices, but we have a rule for doing so.
{{qed}}
Category:Set Union
Category:Well-Orderings
Category:Choice Functions
octuwtzr4d0ejabmufo5r2zpvuqplom
Theorem: Principle of Finite Choice

Let $I$ be a non-empty finite indexing set.
Let $\family {S_i}_{i \mathop \in I}$ be an $I$-indexed family of non-empty sets.
Then there exists an $I$-indexed family $\family {x_i}_{i \mathop \in I}$ such that:
:$\forall i \in I: x_i \in S_i$
That is, there exists a mapping:
:$\ds f: I \to \bigcup_{i \mathop \in I} S_i$
such that:
:$\forall i \in I: \map f i \in S_i$

Proof:
We use the Principle of Mathematical Induction on the cardinality of $I$.
Theorem: Choice Function Exists for Set of Well-Ordered Sets

Let $\mathbb S$ be a set of sets such that:
:$\forall S \in \mathbb S: S \ne \O$
that is, none of the sets in $\mathbb S$ may be empty.
Let every element of $\mathbb S$ be well-ordered.
Then there exists a choice function $f: \mathbb S \to \bigcup \mathbb S$ satisfying:
:$\forall S \in \mathbb S: \exists x \in S: \map f S = x$

Proof:
Every member of $\mathbb S$ is a well-ordered set. 
Thus, for $S \in \mathbb S$, there is a minimal element $s$ for $S$ (with respect to the ordering of $S$). 
By Well-Ordering Minimal Elements are Unique, $s$ is unique.
Therefore, we can define $f$ by:
:$\forall S \in \mathbb S: \map f S = s$
{{qed}}
Theorem: Identity of Power Set with Union

Let $S$ be a set and let $\powerset S$ be its power set.
Consider the algebraic structure $\struct {\powerset S, \cup}$, where $\cup$ denotes set union.
Then the empty set $\O$ serves as the identity for $\struct {\powerset S, \cup}$.

Proof:
From Empty Set is Element of Power Set:
:$\O \in \powerset S$
From Union with Empty Set:
:$\forall A \subseteq S: A \cup \O = A = \O \cup A$
By definition of power set:
:$A \subseteq S \iff A \in \powerset S$
So:
:$\forall A \in \powerset S: A \cup \O = A = \O \cup A$
Thus we see that $\O$ acts as the identity for $\struct {\powerset S, \cup}$.
{{qed}}
Theorem: Identity of Power Set with Intersection

Let $S$ be a set and let $\powerset S$ be its power set.
Consider the algebraic structure $\struct {\powerset S, \cap}$, where $\cap$ denotes set intersection.
Then $S$ serves as the identity for $\struct {\powerset S, \cap}$.

Proof:
We note that by Set is Subset of Itself, $S \subseteq S$ and so $S \in \powerset S$ from the definition of the power set.
From Intersection with Subset is Subset, we have:
:$A \subseteq S \iff A \cap S = A = S \cap A$
By definition of power set:
:$A \subseteq S \iff A \in \powerset S$
So:
:$\forall A \in \powerset S: A \cap S = A = S \cap A$
Thus we see that $S$ acts as the identity element.
{{qed}}
Theorem: Commutation with Inverse in Monoid

Let $x, y \in S$ such that $y$ is invertible.
Then $x$ commutes with $y$ {{iff}} $x$ commutes with $y^{-1}$.

Proof:
=== Necessary Condition ===
Let $x$ commute with $y$.
Then:
{{begin-eqn}}
{{eqn | l = y^{-1} \circ x
      | r = \paren {y^{-1} \circ x} \circ e
      | c = {{MonoidAxiom|2}}
}}
{{eqn | r = y^{-1} \circ \paren {x \circ e}
      | c = {{MonoidAxiom|1}}
}}
{{eqn | r = y^{-1} \circ \paren {x \circ \paren {y \circ y^{-1} } }
      | c = Invertibility of $y$
}}
{{eqn | r = y^{-1} \circ \paren {\paren {x \circ y} \circ y^{-1} }
      | c = {{MonoidAxiom|1}}
}}
{{eqn | r = y^{-1} \circ \paren {\paren {y \circ x} \circ y^{-1} }
      | c = $x$ commutes with $y$
}}
{{eqn | r = \paren {y^{-1} \circ \paren {y \circ x} } \circ y^{-1}
      | c = {{MonoidAxiom|1}}
}}
{{eqn | r = \paren {\paren {y^{-1} \circ y} \circ x} \circ y^{-1}
      | c = {{MonoidAxiom|1}}
}}
{{eqn | r = \paren {e \circ x} \circ y^{-1}
      | c = Invertibility of $y$
}}
{{eqn | r = x \circ y^{-1}
      | c = {{MonoidAxiom|2}}
}}
{{end-eqn}}
So $x$ commutes with $y^{-1}$.
{{Qed|lemma}}
Theorem: Commutation of Inverses in Monoid

Let $x, y \in S$ such that $x$ and $y$ are both invertible.
Then $x$ commutes with $y$ {{iff}} $x^{-1}$ commutes with $y^{-1}$.

Proof:
=== Necessary Condition ===
Let $x$ commute with $y$.
Then:
{{begin-eqn}}
{{eqn | l = x^{-1} \circ y^{-1}
      | r = \paren {y \circ x}^{-1}
      | c = Inverse of Product
}}
{{eqn | r = \paren {x \circ y}^{-1}
      | c =  $x$ commutes with $y$
}}
{{eqn | r = y^{-1} \circ x^{-1}
      | c = Inverse of Product
}}
{{end-eqn}}
So $x^{-1}$ commutes with $y^{-1}$.
{{qed|lemma}}
Theorem: Inverse of Commuting Pair

Let $x, y \in S$ such that $x$ and $y$ are both invertible.
Then $x$ commutes with $y$ {{iff}}:
: $\struct {x \circ y}^{-1} = x^{-1} \circ y^{-1}$

Proof:
{{begin-eqn}}
{{eqn | l = x \circ y
      | r = y \circ x
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = \struct {x \circ y}^{-1}
      | r = \struct {y \circ x}^{-1}
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = \struct {x \circ y}^{-1}
      | r = x^{-1} \circ y^{-1}
      | c = Inverse of Product
}}
{{end-eqn}}
{{Qed}}
Theorem: Conjugate of Commuting Elements

Let $x, y \in S$ such that $x$ and $y$ are both invertible.
Then $x \circ y \circ x^{-1} = y$ {{iff}} $x$ and $y$ commute.

Proof:
As $\struct {S, \circ}$ is a monoid, it is by definition a semigroup.
Therefore it is taken for granted that $\circ$ is associative, so we can dispense with parentheses.
We also take for granted the fact that $x$ and $y$ are cancellable from Invertible Element of Monoid is Cancellable.
So:
{{begin-eqn}}
{{eqn | l = x \circ y
      | r = y \circ x
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = x \circ y \circ x^{-1}
      | r = y \circ x \circ x^{-1}
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = x \circ y \circ x^{-1}
      | r = y
      | c = {{Defof|Invertible Element}}
}}
{{end-eqn}}
{{qed}}
Category:Monoids
Category:Commutativity
Category:Conjugacy
jwpxmdym7615hssmuq1cfwx2xnlvjyb
Theorem: Product of Commuting Elements with Inverses

Let $x, y \in S$ such that $x$ and $y$ are both invertible.
Then:
:$x \circ y \circ x^{-1} \circ y^{-1} = e_S = x^{-1} \circ y^{-1} \circ x \circ y$
{{iff}} $x$ and $y$ commute.

Proof:
As $\struct {S, \circ}$ is a monoid, it is by definition a semigroup.
Therefore $\circ$ is associative, so we can dispense with parentheses.
From Invertible Element of Monoid is Cancellable, we also have that $x, y, x^{-1}, y^{-1}$ are cancellable.
So let :
{{begin-eqn}}
{{eqn | l = x \circ y
      | r = y \circ x
      | c = {{hypothesis}}: $x$ and $y$ commute
}}
{{eqn | ll= \leadstoandfrom
      | l = x \circ y \circ x^{-1}
      | r = y
      | c = Conjugate of Commuting Elements
}}
{{eqn | ll= \leadstoandfrom
      | l = x \circ y \circ x^{-1} \circ y^{-1}
      | r = y \circ y^{-1}
      | c = {{MonoidAxiom|0}}
}}
{{eqn | ll= \leadstoandfrom
      | l = x \circ y \circ x^{-1} \circ y^{-1}
      | r = e_S
      | c = Invertibility of $y$
}}
{{end-eqn}}
Similarly:
{{begin-eqn}}
{{eqn | l = x \circ y
      | r = y \circ x
      | c = {{hypothesis}}: $x$ and $y$ commute
}}
{{eqn | ll= \leadstoandfrom
      | l = y^{-1} \circ x \circ y
      | r = x
      | c = Conjugate of Commuting Elements
}}
{{eqn | ll= \leadstoandfrom
      | l = x^{-1} \circ y^{-1} \circ x \circ y
      | r = x^{-1} \circ x
      | c = {{MonoidAxiom|0}}
}}
{{eqn | ll= \leadstoandfrom
      | l = x^{-1} \circ y^{-1} \circ x \circ y
      | r = e_S
      | c = Invertibility of $x$
}}
{{end-eqn}}
{{qed}}
Category:Monoids
Category:Commutativity
kr5vn5cgulstbooigkhn33k7wz7a85i
Theorem: Exists Element Not in Set

Let $S$ be a set.
Then:
:$\exists x: x \notin S$
That is, for any set, there exists some element which is not in that set.

Proof:
Consider the power set $\powerset S$ of $S$.
{{AimForCont}} $\forall x \in \powerset S: x \in S$.
Then the identity mapping $I_S: S \to \powerset S$ would be a surjection.
But from Cantor's Theorem, there is no surjection $f: S \to \powerset S$.
From this contradiction it follows that:
:$\exists x \in \powerset S: x \notin S$
Hence the result.
{{qed}}
Theorem: Exists Element Not in Set

Let $S$ be a set.
Then:
:$\exists x: x \notin S$
That is, for any set, there exists some element which is not in that set.

Proof:
By the {{Axiom-link|Specification|Sets}}, we can construct the set:
:$T = \set {x \in S: x \notin x}$
Then for all $y$:
:$(*) \quad y \in T$ {{iff}} $\paren {y \in S \land y \notin y}$.
{{AimForCont}} $T \in S$.
By Law of Excluded Middle, either $T \in T$ or $T \notin T$.
Suppose $T \in T$.
By $(*)$, $T \in S \land T \notin T$.
By Rule of Simplification we have $T \notin T$, which is a contradiction.
Now suppose $T \notin T$.
By $(*)$ again, we have $\neg \paren {T \in S \land T \notin T}$.
By Modus Ponendo Tollens, $\neg \paren {T \in S}$, which is also a contradiction.
Hence we must have $T \notin S$.
And thus there exists something (namely $T$) that does not belong to $S$.
{{qed}}
Theorem: Rule of Material Implication

==== Formulation 1 ====
{{:Rule of Material Implication/Formulation 1}}
==== Formulation 2 ====
{{:Rule of Material Implication/Formulation 2}}

Proof:
{{BeginTableau|p \implies q \vdash \neg p \lor q}}
{{Premise|1|p \implies q}}
{{ExcludedMiddle|2|p \lor \neg p}}
{{Assumption|3|\neg p}}
{{Addition|4|3|\neg p \lor q|3|1}}
{{Assumption|5|p}}
{{ModusPonens|6|1, 5|q|1|5}}
{{Addition|7|1, 5|\neg p \lor q|6|2}}
{{ProofByCases|8|1|\neg p \lor q|2|3|4|5|7}}
{{EndTableau}}
{{qed}}
Theorem: Rule of Material Implication

==== Formulation 1 ====
{{:Rule of Material Implication/Formulation 1}}
==== Formulation 2 ====
{{:Rule of Material Implication/Formulation 2}}

Proof:
We apply the Method of Truth Tables.
As can be seen by inspection, the truth values under the main connectives match for all boolean interpretations.
:<nowiki>$\begin {array} {|ccc||cccc|} \hline
p & \implies & q & \neg & p & \lor & q \\
\hline
\F & \T & \F & \T & \F & \T & \F \\
\F & \T & \T & \T & \F & \T & \T \\
\T & \F & \F & \F & \T & \F & \F \\
\T & \T & \T & \F & \T & \T & \T \\
\hline
\end {array}$</nowiki>
{{qed}}
Theorem: Rule of Material Implication

==== Formulation 1 ====
{{:Rule of Material Implication/Formulation 1}}
==== Formulation 2 ====
{{:Rule of Material Implication/Formulation 2}}

Proof:
{{BeginTableau|\neg p \lor q \vdash p \implies q}}
{{Premise|1|\neg p \lor q}}
{{Assumption|2|\neg p|Pick the first of the disjuncts ...}}
{{Assumption|3|p|Assume its negation ...}}
{{NonContradiction|4|2, 3|3|2| ... and demonstrate a contradiction}}
{{Explosion|5|2, 3|q|4| ... from a falsehood, ''any'' statement can be derived - pick $q$}}
{{Implication|6|2|p \implies q|3|5}}
{{Assumption|7|q|Pick the second of the disjuncts ...}}
{{Assumption|8|p|... again assume $p$ ...}}
{{IdentityLaw|9|7|q|7|The truth of $q$ still holds}}
{{Implication|10|7|p \implies q|8|9}}
{{ProofByCases|11|1|p \implies q|1|2|6|7|10}}
{{EndTableau}}
{{qed}}
Theorem: Rule of Material Implication

==== Formulation 1 ====
{{:Rule of Material Implication/Formulation 1}}
==== Formulation 2 ====
{{:Rule of Material Implication/Formulation 2}}

Proof:
{{BeginTableau   |\neg p \lor q \vdash p \implies q}}
{{Premise        |1|\neg p \lor q}}
{{DeMorgan       |2|1|\neg \paren {\neg \neg p \land \neg q}|1|Disjunction}}
{{SequentIntro   |3|1
  |\neg \neg p \implies q
  |2
  |Conditional is Equivalent to Negation of Conjunction with Negative: $\neg \paren {p \land \neg q} \vdash p \implies q$
}}
{{Assumption     |4|p}}
{{DoubleNegIntro |5|4|\neg \neg p|4}}
{{ModusPonens    |6|1, 4|q|3|5}}
{{Implication    |7|1|p \implies q|4|6}}
{{EndTableau|qed}}
Theorem: Rule of Material Implication

==== Formulation 1 ====
{{:Rule of Material Implication/Formulation 1}}
==== Formulation 2 ====
{{:Rule of Material Implication/Formulation 2}}

Proof:
{{BeginTableau|\paren {p \implies q} \iff \paren {\neg p \lor q} }}
{{Assumption|1|p \implies q}}
{{SequentIntro|2|1|\neg p \lor q|1|Rule of Material Implication: Formulation 1}}
{{Implication|3||\paren {p \implies q} \implies \paren {\neg p \lor q}|1|2}}
{{Assumption|4|\neg p \lor q}}
{{SequentIntro|5|4|p \implies q|4|Rule of Material Implication: Formulation 1}}
{{Implication|6||\paren {\neg p \lor q} \implies \paren {p \implies q}|4|5}}
{{BiconditionalIntro|7||\paren {p \implies q} \iff \paren {\neg p \lor q}|3|6}}
{{EndTableau|qed}}
{{LEM|Rule of Material Implication/Formulation 1/Forward Implication|3}}
Theorem: Rule of Material Implication

==== Formulation 1 ====
{{:Rule of Material Implication/Formulation 1}}
==== Formulation 2 ====
{{:Rule of Material Implication/Formulation 2}}

Proof:
We apply the Method of Truth Tables.
As can be seen by inspection, the truth values under the main connective are true for all boolean interpretations.
:<nowiki>$\begin{array}{|ccc|c|cccc|} \hline
(p & \implies & q) & \iff & (\neg & p & \lor & q) \\
\hline
\F & \T & \F & \T & \T & \F & \T & \F \\
\F & \T & \T & \T & \T & \F & \T & \T \\
\T & \F & \F & \F & \T & \T & \F & \F \\
\T & \T & \T & \F & \T & \T & \T & \T \\
\hline
\end{array}$</nowiki>
{{qed}}
Theorem: De Morgan's Laws (Set Theory)/Proof by Induction

Let $\mathbb T = \left\{{T_i: i \mathop \in I}\right\}$, where each $T_i$ is a set and $I$ is some finite indexing set.
Then:

Proof:
Let the cardinality $\card I$ of the indexing set $I$ be $n$.
Then by the definition of cardinality, it follows that $I \cong \N^*_n$ and we can express the proposition:
:$\ds S \setminus \bigcap_{i \mathop \in I} T_i = \bigcup_{i \mathop \in I} \paren {S \setminus T_i}$
as:
:$\ds S \setminus \bigcap_{i \mathop = 1}^n T_i = \bigcup_{i \mathop = 1}^n \paren {S \setminus T_i}$
The proof of this is more amenable to proof by Principle of Mathematical Induction.
For all $n \in \N_{>0}$, let $\map P n$ be the proposition:
:$\ds S \setminus \bigcap_{i \mathop = 1}^n T_i = \bigcup_{i \mathop = 1}^n \paren {S \setminus T_i}$
$\map P 1$ is true, as this just says $S \setminus T_1 = S \setminus T_1$.
=== Base Case ===
$\map P 2$ is the case:
:$S \setminus \paren {T_1 \cap T_2} = \paren {S \setminus T_1} \cup \paren {S \setminus T_2}$
which has been proved. 
This is our basis for the induction.
=== Induction Hypothesis ===
Now we need to show that, if $\map P k$ is true, where $k \ge 2$, then it logically follows that $\map P {k + 1}$ is true.
So this is our induction hypothesis:
:$\ds S \setminus \bigcap_{i \mathop = 1}^k T_i = \bigcup_{i \mathop = 1}^k \paren {S \setminus T_i}$
=== Induction Step ===
Now we need to show:
:$\ds S \setminus \bigcap_{i \mathop = 1}^{k + 1} T_i = \bigcup_{i \mathop = 1}^{k + 1} \paren {S \setminus T_i}$
This is our induction step:
{{begin-eqn}}
{{eqn | l = S \setminus \bigcap_{i \mathop = 1}^{k + 1} T_i
      | r = S \setminus \paren {\bigcap_{i \mathop = 1}^k T_i \cap T_{k + 1} }
      | c = Intersection is Associative
}}
{{eqn | r = \paren {S \setminus \bigcap_{i \mathop = 1}^k T_i} \cup \paren {S \setminus T_{k + 1} }
      | c = Base case
}}
{{eqn | r = \paren {\bigcup_{i \mathop = 1}^k \paren {S \setminus T_i} } \cup \paren {S \setminus T_{k + 1} }
      | c = Induction hypothesis
}}
{{eqn | r = \bigcup_{i \mathop = 1}^{k + 1} \paren {S \setminus T_i}
      | c = Union is Associative
}}
{{end-eqn}}
So $\map P k \implies \map P {k + 1}$ and the result follows by the Principle of Mathematical Induction.
Therefore:
:$\ds S \setminus \bigcap_{i \mathop = 1}^n T_i = \bigcup_{i \mathop = 1}^n \paren {S \setminus T_i}$
that is:
:$\ds S \setminus \bigcap_{i \mathop \in I} T_i = \bigcup_{i \mathop \in I} \paren {S \setminus T_i}$
{{qed}}
Theorem: De Morgan's Laws (Set Theory)/Proof by Induction

Let $\mathbb T = \left\{{T_i: i \mathop \in I}\right\}$, where each $T_i$ is a set and $I$ is some finite indexing set.
Then:

Proof:
Let the cardinality $\size I$ of the indexing set $I$ be $n$.
Then by the definition of cardinality, it follows that $I \cong \N^*_n$ and we can express the proposition:
:$\ds S \setminus \bigcup_{i \mathop \in I} T_i = \bigcap_{i \mathop \in I} \paren {S \setminus T_i}$
as:
:$\ds S \setminus \bigcup_{i \mathop = 1}^n T_i = \bigcap_{i \mathop = 1}^n \paren {S \setminus T_i}$
The proof of this is more amenable to proof by Principle of Mathematical Induction.
For all $n \in \N_{>0}$, let $\map P n$ be the proposition:
:$\ds S \setminus \bigcup_{i \mathop = 1}^n T_i = \bigcap_{i \mathop = 1}^n \paren {S \setminus T_i}$.
$\map P 1$ is true, as this just says $S \setminus T_1 = S \setminus T_1$.
=== Base Case ===
$\map P 2$ is the case:
:$S \setminus \paren {T_1 \cup T_2} = \paren {S \setminus T_1} \cap \paren {S \setminus T_2}$
which has been proved.
This is our basis for the induction.
=== Induction Hypothesis ===
Now we need to show that, if $\map P k$ is true, where $k \ge 2$, then it logically follows that $\map P {k + 1}$ is true.
So this is our induction hypothesis:
:$\ds S \setminus \bigcup_{i \mathop = 1}^k T_i = \bigcap_{i \mathop = 1}^k \paren {S \setminus T_i}$
=== Induction Step ===
Now we need to show:
:$\ds S \setminus \bigcup_{i \mathop = 1}^{k + 1} T_i = \bigcap_{i \mathop = 1}^{k + 1} \paren {S \setminus T_i}$
This is our induction step:
{{begin-eqn}}
{{eqn | l = S \setminus \bigcup_{i \mathop = 1}^{k + 1} T_i
      | r = S \setminus \paren {\bigcup_{i \mathop = 1}^k T_i \cup T_{k + 1} }
      | c = Union is Associative
}}
{{eqn | r = \paren {S \setminus \bigcup_{i \mathop = 1}^k T_i} \cap \paren {S \setminus T_{k + 1} }
      | c = Base case
}}
{{eqn | r = \paren {\bigcap_{i \mathop = 1}^k \paren {S \setminus T_i} } \cap \paren {S \setminus T_{k + 1} }
      | c = Induction hypothesis
}}
{{eqn | r = \bigcap_{i \mathop = 1}^{k + 1} \paren {S \setminus T_i}
      | c = Intersection is Associative
}}
{{end-eqn}}
So $\map P k \implies \map P {k + 1}$ and the result follows by the Principle of Mathematical Induction.
Therefore:
:$\ds S \setminus \bigcup_{i \mathop = 1}^n T_i = \bigcap_{i \mathop = 1}^n \paren {S \setminus T_i}$
that is:
:$\ds S \setminus \bigcup_{i \mathop \in I} T_i = \bigcap_{i \mathop \in I} \paren {S \setminus T_i}$
{{qed}}
Theorem: Union equals Intersection iff Sets are Equal

Let $S$ and $T$ be sets.
Then:
:$\paren {S \cup T = S} \land \paren {S \cap T = S} \iff S = T$
where:
:$S \cup T$ denotes set union
:$S \cap T$ denotes set intersection.

Proof:
From Intersection with Subset is Subset:
:$S \subseteq T \iff S \cap T = S$
From Union with Superset is Superset:
:$S \subseteq T \iff S \cup T = T$
That is:
:$T \subseteq S \iff S \cup T = S$
Thus:
:$\paren {S \cup T = S} \land \paren {S \cap T = S} \iff S \subseteq T \subseteq S$
By definition of set equality:
:$S = T \iff S \subseteq T \subseteq S$
Hence the result.
{{qed}}
Theorem: Intersection with Set Difference is Set Difference with Intersection

: $\left({R \setminus S}\right) \cap T = \left({R \cap T}\right) \setminus S$

Proof:
Consider $R, S, T \subseteq \mathbb U$, where $\mathbb U$ is considered as the universe.
Then:
{{begin-eqn}}
{{eqn | l = \paren {R \setminus S} \cap T
      | r = \paren {R \cap \map \complement S} \cap T
      | c = Set Difference as Intersection with Complement
}}
{{eqn | r = \paren {R \cap T} \cap \map \complement S
      | c = Intersection is Commutative and Intersection is Associative
}}
{{eqn | r = \paren {R \cap T} \setminus S
      | c = Set Difference as Intersection with Complement
}}
{{end-eqn}}
{{qed}}
Theorem: Intersection with Set Difference is Set Difference with Intersection

: $\left({R \setminus S}\right) \cap T = \left({R \cap T}\right) \setminus S$

Proof:
{{begin-eqn}}
{{eqn | o = 
      | r = x \in \paren {R \setminus S} \cap T
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | o = 
      | r = \paren {x \in R \land x \notin S} \land x \in T
      | c = {{Defof|Set Intersection}} and {{Defof|Set Difference}}
}}
{{eqn | ll= \leadstoandfrom
      | o = 
      | r = \paren {x \in R \land x \in T} \land x \notin S
      | c = Rule of Commutation and Rule of Association
}}
{{eqn | ll= \leadstoandfrom
      | o = 
      | r = x \in \paren {R \cap T} \setminus S
      | c = {{Defof|Set Intersection}} and {{Defof|Set Difference}}
}}
{{end-eqn}}
{{qed}}
Theorem: Set Difference is Right Distributive over Set Intersection

:$\paren {A \cap B} \setminus C = \paren {A \setminus C} \cap \paren {B \setminus C}$

Proof:
{{begin-eqn}}
{{eqn | l = x
      | o = \in
      | r = \bigcap_{X \mathop \in U} \paren {X \setminus T}
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | q = \forall X \in U
      | l = x
      | o = \in
      | r = X \setminus T
      | c = {{Defof|Set Intersection}}
}}
{{eqn | ll= \leadstoandfrom
      | q = \forall X \in U
      | l = x
      | o = \in
      | r = X
      | c = {{Defof|Set Difference}}
}}
{{eqn | lo= \land
      | l = x
      | o = \not \in
      | r = T
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | o = \in
      | r = \bigcap_{X \mathop \in U}
      | c = {{Defof|Set Intersection}}
}}
{{eqn | lo= \land 
      | l = x
      | o = \not \in
      | r = T
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | o = \in
      | r = \paren {\bigcap_{X \mathop \in U} X} \setminus T
      | c = {{Defof|Set Difference}}
}}
{{end-eqn}}
{{qed}}