avewright/proofwiki-math huggingface dataset:
Theorem: Intersection Distributes over Symmetric Difference

Intersection is distributive over symmetric difference:
{{begin-eqn}}
{{eqn | l = \paren {R \symdif S} \cap T
      | r = \paren {R \cap T} \symdif \paren {S \cap T}
}}
{{eqn | l = T \cap \paren {R \symdif S}
      | r = \paren {T \cap R} \symdif \paren {T \cap S}
}}
{{end-eqn}}

Proof:
From Set Intersection Distributes over Set Difference, we have:
:$\paren {R \setminus S} \cap T = \paren {R \cap T} \setminus \paren {S \cap T}$
So:
{{begin-eqn}}
{{eqn | l = \paren {R \cap T} \symdif \paren {S \cap T}
      | r = \paren {\paren {R \cap T} \setminus \paren {S \cap T} } \cup \paren {\paren {S \cap T} \setminus \paren {R \cap T} }
      | c = {{Defof|Symmetric Difference}}
}}
{{eqn | r = \paren {\paren {R \setminus S} \cap T} \cup \paren {\paren {S \setminus R} \cap T}
      | c = Set Intersection Distributes over Set Difference
}}
{{eqn | r = \paren {\paren {R \setminus S} \cup \paren {S \setminus R} } \cap T
      | c = Intersection Distributes over Union
}}
{{eqn | r = \paren {R \symdif S} \cap T
      | c = {{Defof|Symmetric Difference}}
}}
{{end-eqn}}
The second part of the proof is a direct consequence of the fact that Intersection is Commutative.
{{qed}}
Theorem: Symmetric Difference of Unions

Let $R$, $S$ and $T$ be sets.
Then:
:$\paren {R \cup T} \symdif \paren {S \cup T} = \paren {R \symdif S} \setminus T$
where:
:$\symdif$ denotes the symmetric difference
:$\setminus$ denotes set difference
:$\cup$ denotes set union

Proof:
{{begin-eqn}}
{{eqn | l = \paren {R \cup T} \symdif \paren {S \cup T}
      | r = \paren {\paren {R \cup T} \setminus \paren {S \cup T} } \cup \paren {\paren {S \cup T} \setminus \paren {R \cup T} }
      | c = {{Defof|Symmetric Difference|index = 1}}
}}
{{eqn | r = \paren {\paren {R \setminus S} \setminus T} \cup \paren {\paren {S \setminus R} \setminus T}
      | c = Set Difference with Union
}}
{{eqn | r = \paren {\paren {R \setminus S} \cup \paren {S \setminus R} } \setminus T
      | c = Set Difference is Right Distributive over Union
}}
{{eqn | r = \paren {R \symdif S} \setminus T
      | c = {{Defof|Symmetric Difference|index = 1}}
}}
{{end-eqn}}
{{Qed}}
Category:Symmetric Difference
Category:Set Union
pxk5a2vhipfne1v1ox0it3psj4bdj26
Theorem: Intersection with Universal Set

The intersection of a set with the universal set is the set itself:
:$\mathbb U \cap S = S$

Proof:
{{begin-eqn}}
{{eqn | l = S
      | o = \subseteq
      | r = \mathbb U
      | c = {{Defof|Universal Set}}
}}
{{eqn | ll= \leadstoandfrom
      | l = \mathbb U \cap S
      | r = S
      | c = Intersection with Subset is Subset
}}
{{end-eqn}}
{{qed}}
Theorem: Union with Universal Set

The union of a set with the universal set is the universal set:
:$\mathbb U \cup S = \mathbb U$

Proof:
{{begin-eqn}}
{{eqn | l = S
      | o = \subseteq
      | r = \mathbb U
      | c = {{Defof|Universal Set}}
}}
{{eqn | ll= \leadstoandfrom
      | l = \mathbb U \cup S
      | r = \mathbb U
      | c = Union with Superset is Superset
}}
{{end-eqn}}
{{qed}}
Theorem: Complement of Empty Set is Universal Set

The complement of the empty set is the universal set:
:$\map \complement \O = \mathbb U$

Proof:
Substitute $\mathbb U$ for $S$ in $\relcomp S \O = S$ from Relative Complement of Empty Set.
{{qed}}
Theorem: Complement of Universal Set is Empty Set

The complement of the universal set is the empty set:
:$\map \complement {\mathbb U} = \O$

Proof:
Substitute $\mathbb U$ for $S$ in $\relcomp S S = \O$ from Relative Complement with Self is Empty Set.
{{Qed}}
Theorem: Complement of Complement

The complement of the complement of a set is the set itself:
:$\map \complement {\map \complement S} = S$

Proof:
Substitute $\mathbb U$ for $S$ and $S$ for $T$ in $\relcomp S {\relcomp S T} = T$ from Relative Complement of Relative Complement.
{{qed}}
Theorem: Intersection with Complement

The intersection of a set and its complement is the empty set:
:$S \cap \map \complement S = \O$

Proof:
Substitute $\mathbb U$ for $S$ and $S$ for $T$ in $T \cap \relcomp S T = \O$ from Intersection with Relative Complement is Empty.
{{qed}}
Theorem: Union with Complement

The union of a set and its complement is the universal set:
:$S \cup \map \complement S = \mathbb U$

Proof:
Substitute $\mathbb U$ for $S$ and $S$ for $T$ in $T \cup \relcomp S T = S$ from Union with Relative Complement.
{{qed}}
{{LEM|Union with Relative Complement}}
Theorem: Set with Complement forms Partition

Let $\O \subset S \subset \mathbb U$.
Then $S$ and its complement $\map \complement S$ form a partition of the universal set $\mathbb U$.

Proof:
Follows directly from Set with Relative Complement forms Partition:
If $\O \subset T \subset S$, then $\set {T, \relcomp S T}$ is a partition of $S$.
{{Qed}}
Category:Set Complement
Category:Universal Set
Category:Set Partitions
6sxbs5qe78y1wegwid1kahz3yitbtoj
Theorem: Set Difference as Intersection with Complement

Set difference can be expressed as the intersection with the set complement:
:$A \setminus B = A \cap \map \complement B$

Proof:
This follows directly from Set Difference as Intersection with Relative Complement:
:$A \setminus B = A \cap \relcomp S B$
Let $S = \Bbb U$.
Since $A, B \subseteq \Bbb U$ by definition of the universal set, the result follows.
{{qed}}
Theorem: Set Difference of Complements

:$\map \complement S \setminus \map \complement T = T \setminus S$

Proof:
{{begin-eqn}}
{{eqn | l = \map \complement S \setminus \map \complement T
      | r = \set {x: x \in \map \complement S \land x \notin \map \complement T}
      | c = {{Defof|Set Difference}}
}}
{{eqn | r = \set {x: x \notin S \land x \in T}
      | c = {{Defof|Set Complement}}
}}
{{eqn | r = \set {x: x \in T \land x \notin S}
      | c = Rule of Commutation
}}
{{eqn | r = T \setminus S
      | c = {{Defof|Set Difference}}
}}
{{end-eqn}}
{{qed}}
Category:Set Difference
Category:Set Complement
8od5ab3u9f9ipanyue0hqjkci734s8n
Theorem: Symmetric Difference of Complements

The symmetric difference of two sets equals the symmetric difference of their complements:
:$\map \complement S \symdif \map \complement T = S \symdif T$

Proof:
{{begin-eqn}}
{{eqn | l = \map \complement S \symdif \map \complement T
      | r = \paren {\map \complement S \setminus \map \complement T} \cup \paren {\map \complement T \setminus \map \complement S}
      | c = {{Defof|Symmetric Difference}}
}}
{{eqn | r = \paren {T \setminus S} \cup \paren {S \setminus T}
      | c = Set Difference of Complements
}}
{{eqn | r = S \symdif T
      | c = {{Defof|Symmetric Difference}}
}}
{{end-eqn}}
{{qed}}
Theorem: Symmetric Difference with Universal Set

:$\mathbb U \symdif S = \map \complement S$
where:
:$\mathbb U$ denotes the universal set
:$\symdif$ denotes symmetric difference.

Proof:
{{begin-eqn}}
{{eqn | l = \mathbb U \symdif S
      | r = \mathbb U \cup S \setminus \mathbb U \cap S
      | c = {{Defof|Symmetric Difference|index = 2}}
}}
{{eqn | r = \mathbb U \cup S \setminus S
      | c = Intersection with Universal Set
}}
{{eqn | r = \mathbb U \setminus S
      | c = Union with Universal Set
}}
{{eqn | r = \map \complement S
      | c = {{Defof|Set Complement}}
}}
{{end-eqn}}
{{qed}}
Theorem: Symmetric Difference with Self is Empty Set

The symmetric difference of a set with itself is the empty set:
:$S \symdif S = \O$

Proof:
This follows directly from Symmetric Difference of Equal Sets:
:$S \symdif T = \O \iff S = T$
substituting $S$ for $T$.
{{Qed}}
Theorem: Symmetric Difference with Complement

The symmetric difference of a set with its complement is the universal set:
:$S \symdif \relcomp {} S = \mathbb U$

Proof:
{{begin-eqn}}
{{eqn | l = S \symdif \relcomp {} S
      | r = \paren {S \cup \relcomp {} S} \setminus \paren {S \cap \relcomp {} S}
      | c = {{Defof|Symmetric Difference|index = 2}}
}}
{{eqn | r = \paren {S \cup \relcomp {} S} \setminus \O
      | c = Intersection with Complement
}}
{{eqn | r = \mathbb U \setminus \O
      | c = Union with Complement
}}
{{eqn | r = \mathbb U
      | c = Set Difference with Empty Set is Self
}}
{{end-eqn}}
{{qed}}
Theorem: Symmetric Difference is Associative

Symmetric difference is associative:
:$R \symdif \paren {S \symdif T} = \paren {R \symdif S} \symdif T$

Proof:
We can directly expand the expressions for $R \symdif \paren {S \symdif T}$ and $\paren {R \symdif S} \symdif T$, and see that they come to the same thing.
Expanding the {{RHS}}:
{{begin-eqn}}
{{eqn | o = 
      | r = \paren {R \symdif S} \symdif T
      | c = 
}}
{{eqn | r = \paren {\paren {\paren {R \cap \overline S} \cup \paren {\overline R \cap S} } \cap \overline T} \cup \paren {\overline {R \symdif S} \cap T}
      | c = {{Defof|Symmetric Difference|index = 3}}
}}
{{eqn | r = \paren {\paren {\paren {R \cap \overline S} \cup \paren {\overline R \cap S} } \cap \overline T} \cup \paren {\overline {\paren {\paren {R \cup S} \cap \paren {\overline R \cup \overline S} } } \cap T}
      | c = {{Defof|Symmetric Difference|index = 4}}
}}
{{eqn | r = \paren {R \cap \overline S \cap \overline T} \cup \paren {\overline R \cap S \cap \overline T} \cup \paren {\paren {\overline {\paren {R \cup S} } \cup \overline {\paren {\overline R \cup \overline S} } } \cap T}
      | c = Intersection Distributes over Union and De Morgan
}}
{{eqn | r = \paren {R \cap \overline S \cap \overline T} \cup \paren {\overline R \cap S \cap \overline T} \cup \paren {\paren {\paren {\overline R \cap \overline S} \cup \paren {R \cap S} } \cap T}
      | c = De Morgan
}}
{{eqn | r = \paren {R \cap \overline S \cap \overline T} \cup \paren {\overline R \cap S \cap \overline T} \cup \paren {\overline R \cap \overline S \cap T} \cup \paren {R \cap S \cap T}
      | c = Intersection Distributes over Union
}}
{{end-eqn}}
Expanding the {{LHS}}:
{{begin-eqn}}
{{eqn | o = 
      | r = R \symdif \paren {S \symdif T}
      | c = 
}}
{{eqn | r = \paren {R \cap \overline {S \symdif T} } \cup \paren {\overline R \cap \paren {\paren {S \cap \overline T} \cup \paren {\overline S \cap T} } }
      | c = {{Defof|Symmetric Difference|index = 3}}
}}
{{eqn | r = \paren {R \cap \overline {\paren {\paren {S \cup T} \cap \paren {\overline S \cup \overline T} } } } \cup \paren {\overline R \cap \paren {\paren {S \cap \overline T} \cup \paren {\overline S \cap T} } }
      | c = {{Defof|Symmetric Difference|index = 4}}
}}
{{eqn | r = \paren {R \cap \paren {\overline {\paren {S \cup T} } \cup \overline {\paren {\overline S \cup \overline T} } } } \cup \paren {\overline R \cap S \cap \overline T} \cup \paren {\overline R \cap \overline S \cap T}
      | c = Intersection Distributes over Union and De Morgan
}}
{{eqn | r = \paren {R \cap \paren {\paren {\overline S \cap \overline T} \cup \paren {S \cap T} } } \cup \paren {\overline R \cap S \cap \overline T} \cup \paren {\overline R \cap \overline S \cap T}
      | c = De Morgan
}}
{{eqn | r = \paren {R \cap \overline S \cap \overline T} \cup \paren {R \cap S \cap T} \cup \paren {\overline R \cap S \cap \overline T} \cup \paren {\overline R \cap \overline S \cap T}
      | c = Intersection Distributes over Union
}}
{{end-eqn}}
From Union is Commutative it is seen that the {{LHS}} and {{RHS}} are the same, and the result is proved.
{{qed}}
Theorem: Symmetric Difference is Associative

Symmetric difference is associative:
:$R \symdif \paren {S \symdif T} = \paren {R \symdif S} \symdif T$

Proof:
Expanding the {{RHS}}:
{{begin-eqn}}
{{eqn | o = 
      | r = \paren {R \symdif S} \symdif T
      | c = 
}}
{{eqn | r = \paren {\paren {\paren {R \cup S} \cap \paren {\overline R \cup \overline S} } \cup T} \cap \paren {\overline {R \symdif S} \cup \overline T}
      | c = {{Defof|Symmetric Difference|index = 4}}
}}
{{eqn | r = \paren {\paren {\paren {R \cup S} \cap \paren {\overline R \cup \overline S} } \cup T} \cap \paren {\overline {\paren {\paren {R \cap \overline S} \cup \paren {\overline R \cap S} } } \cup \overline T}
      | c = {{Defof|Symmetric Difference|index = 3}}
}}
{{eqn | r = \paren {R \cup S \cup T} \cap \paren {\overline R \cup \overline S \cup T} \cap \paren {\paren {\overline {\paren {R \cap \overline S} } \cap \overline {\paren {\overline R \cap S} } } \cup \overline T}
      | c = Union Distributes over Intersection and De Morgan
}}
{{eqn | r = \paren {R \cup S \cup T} \cap \paren {\overline R \cup \overline S \cup T} \cap \paren {\paren {\paren {\overline R \cup S} \cap \paren {R \cup \overline S} } \cup \overline T}
      | c = De Morgan
}}
{{eqn | r = \paren {R \cup S \cup T} \cap \paren {\overline R \cup \overline S \cup T} \cap \paren {\overline R \cup S \cup \overline T} \cap \paren {R \cup \overline S \cup \overline T}
      | c = Union Distributes over Intersection
}}
{{end-eqn}}
Expanding the {{LHS}}:
{{begin-eqn}}
{{eqn | o = 
      | r = R \symdif \paren {S \symdif T}
      | c = 
}}
{{eqn | r = \paren {R \cup \paren {\paren {S \cup T} \cap \paren {\overline S \cup \overline T} } } \cap \paren {\overline R \cup \overline {S \symdif T} }
      | c = {{Defof|Symmetric Difference|index = 4}}
}}
{{eqn | r = \paren {R \cup \paren {\paren {S \cup T} \cap \paren {\overline S \cup \overline T} } } \cap \paren {\overline R \cup \overline {\paren {\paren {S \cap \overline T} \cup \paren {\overline S \cap T} } } }
      | c = {{Defof|Symmetric Difference|index = 3}}
}}
{{eqn | r = \paren {R \cup S \cup T} \cap \paren {R \cup \overline S \cup \overline T} \cap \paren {\overline R \cup \paren {\overline {\paren {S \cap \overline T} } \cap \overline {\paren {\overline S \cap T} } } }
      | c = Union Distributes over Intersection and De Morgan
}}
{{eqn | r = \paren {R \cup S \cup T} \cap \paren {R \cup \overline S \cup \overline T} \cap \paren {\overline R \cup \paren {\paren {\overline S \cup T} \cap \paren {S \cup \overline T} } }
      | c = De Morgan
}}
{{eqn | r = \paren {R \cup S \cup T} \cap \paren {R \cup \overline S \cup \overline T} \cap \paren {\overline R \cup \overline S \cup T} \cap \paren {\overline R \cup S \cup \overline T}
      | c = Union Distributes over Intersection
}}
{{end-eqn}}
From Intersection is Commutative, it can be seen that the {{LHS}} and {{RHS}} are the same, and the result is proved.
{{qed}}
Theorem: Cartesian Product is Empty iff Factor is Empty

:$S \times T = \O \iff S = \O \lor T = \O$
Thus:
:$S \times \O = \O = \O \times T$

Proof:
{{begin-eqn}}
{{eqn | l = S \times T
      | o = \ne
      | r = \O
}}
{{eqn | ll= \leadstoandfrom
      | l = \exists \tuple {s, t}
      | o = \in
      | r = S \times T
      | c = {{Defof|Empty Set}}
}}
{{eqn | ll= \leadstoandfrom
      | l = \exists s \in S
      | o = \land
      | r = \exists t \in T
      | c = {{Defof|Cartesian Product}}
}}
{{eqn | ll= \leadstoandfrom
      | l = S \ne \O
      | o = \land
      | r = T \ne \O
      | c = {{Defof|Empty Set}}
}}
{{eqn | ll= \leadstoandfrom
      | l = \neg \leftparen {S = \O}
      | o = \lor
      | r = \rightparen {T = \O}
      | c = De Morgan's Laws: Conjunction of Negations
}}
{{end-eqn}}
So by the Rule of Transposition:
:$S = \O \lor T = \O \iff S \times T = \O$
{{Qed}}
Theorem: Cartesian Product is Anticommutative

Let $S, T \ne \O$.
Then:
:$S \times T = T \times S \iff S = T$

Proof:
Suppose $S \times T = T \times S$.
Then:
{{begin-eqn}}
{{eqn | l = x \in S
      | o = \land
      | r = y \in T
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = \tuple {x, y}
      | o = \in
      | r = S \times T
      | c = {{Defof|Cartesian Product}}
}}
{{eqn | ll= \leadstoandfrom
      | l = \tuple {x, y}
      | o = \in
      | r = T \times S
      | c = {{hypothesis}}
}}
{{eqn | ll= \leadstoandfrom
      | l = x \in T
      | o = \land
      | r = y \in S
      | c = {{Defof|Cartesian Product}}
}}
{{end-eqn}}
Thus it can be seen from the definition of set equality that $S \times T = T \times S \iff S = T$.
Note that if $S = \O$ or $T = \O$ then, from Cartesian Product is Empty iff Factor is Empty, $S \times T = T \times S = \O$ whatever $S$ and $T$ are, and the result does not hold.
{{qed}}
Theorem: Cartesian Product of Subsets

Let $A, B, S, T$ be sets such that $A \subseteq B$ and $S \subseteq T$.
Then:
:$A \times S \subseteq B \times T$
In addition, if $A, S \ne \O$, then:
:$A \times S \subseteq B \times T \iff A \subseteq B \land S \subseteq T$

Proof:
First we show that $A \subseteq B \land S \subseteq T \implies A \times S \subseteq B \times T$.
First, let $A = \O$ or $S = \O$.
Then from Cartesian Product is Empty iff Factor is Empty:
:$A \times S = \O \subseteq B \times T$
so the result holds.
Next, let $A, S \ne \O$.
Then from Cartesian Product is Empty iff Factor is Empty:
:$A \times S \ne \O$
and we can use the following argument:
{{begin-eqn}}
{{eqn | o =
      | r = \tuple {x, y} \in A \times S
}}
{{eqn | o = \leadsto
      | r = x \in A, y \in S
      | c = {{Defof|Cartesian Product}}
}}
{{eqn | o = \leadsto
      | r = x \in B, y \in T
      | c = {{Defof|Subset}}
}}
{{eqn | o = \leadsto
      | r = \tuple {x, y} \in B \times T
      | c = {{Defof|Cartesian Product}}
}}
{{end-eqn}}
Thus $A \times S \subseteq B \times T$ as we were to prove.
Now we show that if $A, S \ne \O$, then:
:$A \times S \subseteq B \times T \implies A \subseteq B \land S \subseteq T$
So suppose that $A \times S \subseteq B \times T$.
First note that if $A = \O$, then $A \times S = \O \subseteq B \times T$, whatever $S$ is, so it is not necessarily the case that $S \subseteq T$.
Similarly if $S = \O$; it is not necessarily the case that $A \subseteq B$.
So that explains the restriction $A, S \ne \O$.
Now, as $A, S \ne \O$, $\exists x \in A, y \in S$.
Thus:
{{begin-eqn}}
{{eqn | o =
      | r = x \in A, y \in S
}}
{{eqn | o = \leadsto
      | r = \tuple {x, y} \in A \times S
      | c = {{Defof|Cartesian Product}}
}}
{{eqn | o = \leadsto
      | r = \tuple {x, y} \in B \times T
      | c = {{Defof|Subset}}
}}
{{eqn | o = \leadsto
      | r = x \in B, y \in T
      | c = {{Defof|Cartesian Product}}
}}
{{end-eqn}}
So when $A, S \ne \O$, we have:
:$A \subseteq S \land B \subseteq T \implies A \times S \subseteq B \times T$
:$A \times S \subseteq B \times T \implies A \subseteq B \land S \subseteq T$
from which:
:$A \times S \subseteq B \times T \iff A \subseteq B \land S \subseteq T$
{{qed}}
Theorem: Cartesian Product of Intersections

:$\paren {S_1 \cap S_2} \times \paren {T_1 \cap T_2} = \paren {S_1 \times T_1} \cap \paren {S_2 \times T_2}$
where $S_1, S_2, T_1, T_2$ are sets.

Proof:
{{begin-eqn}}
{{eqn | o = 
      | r = \tuple {x, y} \in \paren {S_1 \cap S_2} \times \paren {T_1 \cap T_2}
}}
{{eqn | o = \leadstoandfrom
      | r = \paren {x \in S_1 \land x \in S_2} \land \paren {y \in T_1 \land y \in T_2}
      | c = {{Defof|Cartesian Product}} and {{Defof|Set Intersection}}
}}
{{eqn | o = \leadstoandfrom
      | r = \paren {x \in S_1 \land y \in T_1} \land \paren {x \in S_2 \land y \in T_2}
      | c = Rule of Commutation, Rule of Association
}}
{{eqn | o = \leadstoandfrom
      | r = \tuple {x, y} \in S_1 \times T_1 \land \tuple {x, y} \in S_2 \times T_2
      | c = {{Defof|Cartesian Product}}
}}
{{eqn | o = \leadstoandfrom
      | r = \tuple {x, y} \in \paren {S_1 \times T_1} \cap \paren {S_2 \times T_2}
      | c = {{Defof|Set Intersection}}
}}
{{end-eqn}}
{{qed}}
Theorem: Cartesian Product Distributes over Union

Cartesian product is distributive over union:
:$A \times \paren {B \cup C} = \paren {A \times B} \cup \paren {A \times C}$
:$\paren {B \cup C} \times A = \paren {B \times A} \cup \paren {C \times A}$

Proof:
Take the result Cartesian Product of Unions:
:$\paren {S_1 \cup S_2} \times \paren {T_1 \cup T_2} = \paren {S_1 \times T_1} \cup \paren {S_2 \times T_2} \cup \paren {S_1 \times T_2} \cup \paren {S_2 \times T_1}$
Put $S_1 = S_2 = A, T_1 = B, T_2 = C$:
{{begin-eqn}}
{{eqn | o = 
      | r = A \times \paren {B \cup C}
      | c = 
}}
{{eqn | r = \paren {A \cup A} \times \paren {B \cup C}
      | c = Set Union is Idempotent
}}
{{eqn | r = \paren {A \times B} \cup \paren {A \times C} \cup \paren {A \times C} \cup \paren {A \times B}
      | c = Cartesian Product of Unions
}}
{{eqn | r = \paren {A \times B} \cup \paren {A \times C}
      | c = Set Union is Idempotent
}}
{{end-eqn}}
Thus:
:$A \times \paren {B \cup C} = \paren {A \times B} \cup \paren {A \times C}$
The other result is proved similarly.
{{qed}}
Theorem: Cartesian Product of Unions

:$\paren {A \cup B} \times \paren {C \cup D} = \paren {A \times C} \cup \paren {B \times D} \cup \paren {A \times D} \cup \paren {B \times C}$

Proof:
{{begin-eqn}}
{{eqn | o = 
      | r = \tuple {x, y} \in \paren {A \cup B} \times \paren {C \cup D}
}}
{{eqn | ll= \leadstoandfrom
      | o = 
      | r = \paren {x \in A \lor x \in B}
}}
{{eqn | o = \land
      | r = \paren {y \in C \lor y \in D}
      | c = {{Defof|Cartesian Product}} and {{Defof|Set Union}}
}}
{{eqn | ll= \leadstoandfrom
      | o = 
      | r = \paren {\paren {x \in A \lor x \in B} \land y \in C}
}}
{{eqn | o = \lor
      | r = \paren {\paren {x \in A \lor x \in B} \land y \in D}
      | c = Rule of Distribution
}}
{{eqn | ll= \leadstoandfrom
      | o = 
      | r = \paren {x \in A \land y \in C}
}}
{{eqn | o = \lor
      | r = \paren {x \in B \land y \in C}
}}
{{eqn | o = \lor
      | r = \paren {x \in A \land y \in D}
}}
{{eqn | o = \lor
      | r = \paren {x \in B \land y \in D}
      | c = Rule of Distribution
}}
{{eqn | ll= \leadstoandfrom
      | o = 
      | r = \tuple {x, y} \in \paren {A \times C} \cup \paren {B \times D} \cup \paren {A \times D} \cup \paren {B \times C}
      | c = {{Defof|Cartesian Product}} and {{Defof|Set Union}}
}}
{{end-eqn}}
{{qed}}
Theorem: Cartesian Product Distributes over Set Difference

Cartesian product is distributive over set difference:
:$(1): \quad S \times \paren {T_1 \setminus T_2} = \paren {S \times T_1} \setminus \paren {S \times T_2}$
:$(2): \quad \paren {T_1 \setminus T_2} \times S = \paren {T_1 \times S} \setminus \paren {T_2 \times S}$

Proof:
{{begin-eqn}}
{{eqn | o = 
      | r = \tuple {x, y} \in S \times \paren {T_1 \setminus T_2}
      | c = 
}}
{{eqn | o = \leadstoandfrom
      | r = \paren {x \in S} \land \paren {y \in \paren {T_1 \setminus T_2} }
      | c = {{Defof|Cartesian Product}}
}}
{{eqn | o = \leadstoandfrom
      | r = \paren {x \in S} \land \paren {y \in T_1} \land \paren {y \notin T_2}
      | c = {{Defof|Set Difference}}
}}
{{eqn | o = \leadstoandfrom
      | r = \paren {\tuple {x, y} \in S \times T_1} \land \paren {\tuple {x, y} \notin S \times T_2}
      | c = {{Defof|Cartesian Product}}
}}
{{eqn | o = \leadstoandfrom
      | r = \tuple {x, y} \in \paren {S \times T_1} \setminus \paren {S \times T_2}
      | c = {{Defof|Set Difference}}
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | o = 
      | r = \tuple {x, y} \in \paren {T_1 \setminus T_2} \times S
      | c = 
}}
{{eqn | o = \leadstoandfrom
      | r = \paren {x \in \paren {T_1 \setminus T_2} } \land \paren {y \in S}
      | c = {{Defof|Cartesian Product}}
}}
{{eqn | o = \leadstoandfrom
      | r = \paren {x \in T_1} \land \paren {x \notin T_2} \land \paren {y \in S}
      | c = {{Defof|Set Difference}}
}}
{{eqn | o = \leadstoandfrom
      | r = \paren {\tuple {x, y} \in T_1 \times S} \land \paren {\tuple {x, y} \notin T_2 \times S}
      | c = {{Defof|Cartesian Product}}
}}
{{eqn | o = \leadstoandfrom
      | r = \tuple {x, y} \in \paren {T_1 \times S} \setminus \paren {T_2 \times S}
      | c = {{Defof|Set Difference}}
}}
{{end-eqn}}
{{Qed}}