Solution (source code)

= Solution

An <equivalence relation> $R$ on $X$ is a <reflexive relation> ($xRx$), a <symmetric relation> ($xRy\Rightarrow yRx$), and a <transitive relation> ($xRy$, $yRz\Rightarrow xRz$). Its <equivalence class> at $x$ is $[x]_R=\{y\in X:xRy\}$. Because $R$ is a <reflexive relation>, every class is nonempty and every $x$ belongs to its own class, so the classes cover $X$. If $[x]_R$ and $[z]_R$ share an element $y$, symmetry and <transitivity> give $xRz$. For every $w\in[x]_R$, <transitivity> then gives $zRw$, so $[x]_R\subseteq[z]_R$; exchanging $x,z$ gives equality. Thus distinct classes are disjoint. \b[The equivalence classes form a <set partition> of $X$.] On the <empty set>, the empty family is the corresponding partition.