DEF-ROS. Roster Notation / Enumeration Notation.
We define
\[\begin{align*} \{a,b,c\} &= \{a,b\}\cup\{c\}, \\ \{a,b,c,d\} &= \{a,b,c\}\cup\{d\}, \end{align*}\]and so on.
PROP-ROS.
For any $a_1$, $\cdots$, $a_n$ ($n\geq 1$),
\[\forall x :\enspace x\in\{a_1,\cdots,a_n\} \enspace\Leftrightarrow\enspace x=a_1\lor\cdots\lor x=a_n.\]