DEF-ITSC. Intersection.
The intersection of $X$ is
\[\bigcap X = \left\{x\in\bigcup X : (\forall Y\in X:x\in Y)\right\}.\]For any $A$ and $B$, we define
\[A\cap B = \bigcap\{A,B\}.\]For any $A$, $B$ and $C$, we define
\[A\cap B\cap C = (A\cap B)\cap C,\]and so on.
PROP-ITSC-SUB.
For any $X$,
\[\bigcap X \subseteq \bigcup X.\]
PROP-ITSC-EMP.
\[\bigcap\varnothing = \varnothing.\]
PROP-ITSC-EMP2.
For any $X$,
\[X\cap\varnothing = \varnothing.\]
PROP-ITSC-SLF.
For any $X$,
\[X\cap X = X.\]
PROP-ITSC-COM. Commutativity.
For any $A$ and $B$,
\[A\cap B = B\cap A.\]
PROP-ITSC-ASS. Associativity.
For any $A$, $B$ and $C$,
\[(A\cap B)\cap C = A\cap (B\cap C).\]