DEF-SUB. Subset.
$X$ is a subset of $Y$, written $X\subseteq Y$, if
\[\forall x :\enspace x\in X \enspace\Rightarrow\enspace x\in Y.\]$X$ is a proper subset of $Y$, written $X\subset Y$, if $X\subseteq Y$ and $X\neq Y$.
PROP-SUB-EMP.
$\varnothing$ is the only set that is a subset of any set. That is, for any $X$,
\[X=\varnothing \enspace\Leftrightarrow\enspace \forall Y:X\subseteq Y.\]
PROP-SUB-REF. Reflexivity of $\subseteq$.
For any $X$,
\[X\subseteq X.\]
PROP-SUB-TR. Transitivity of $\subseteq$.
For any $X$, $Y$ and $Z$,
\[X\subseteq Y\land Y\subseteq Z \enspace\Rightarrow\enspace X\subseteq Z.\]
PROP-SUB-ATSYM. Antisymmetry of $\subseteq$.
For any $X$ and $Y$,
\[X\subseteq Y\land Y\subseteq X \enspace\Rightarrow\enspace X=Y.\]
PROP-SUB-PO.
For any $X$, if we let
\[{\subseteq_X} = \{(x,y)\in X\times X:x\subseteq y\},\]then $\subseteq_X$ is a reflexive, transitive and antisymmetric relation (DEF-RP), which menas $\subseteq_X$ is a partial order.
PROP-SUB-PIREF. Irreflexivity of $\subset$.
For any $X$,
\[X\not\subset X.\]
PROP-SUB-PTR. Transitivity of $\subset$.
For any $X$, $Y$ and $Z$,
\[X\subset Y\land Y\subset Z \enspace\Rightarrow\enspace X\subset Z.\]
PROP-SUB-PASYM. Asymmetry of $\subset$.
For any $X$ and $Y$,
\[X\subset Y \enspace\Rightarrow\enspace Y\not\subset X.\]
PROP-SUB-SPO.
For any $X$, if we let
\[{\subset_X} = \{(x,y)\in X\times X:x\subset y\},\]then $\subset$ is an irreflexive, transitive and asymmetric relation (DEF-RP), which means $\subset$ is a strict partial order.