非順序対の定義

次の記述は,$x$一つだけからなる集合$\{x\}$と $x,y$という二つの要素をもつ集合$\{y,z\}$の定義です。

 definition let y; func { y } means
  x in it iff x = y;
  correctness;
  let z; func { y, z } means
   x in it iff x = y or x = z;
  correctness;
  commutativity;
 end;

任意の$y$に対して$\{y\}$とは,任意の$x$について

$$x \in \{y\} \Leftrightarrow x = y$$

を充たす集合であり,

任意の$y,z$に対して$\{y,z\}$とは,任意の$x$について

$$x \in \{y,z\} \Leftrightarrow x = y \ or \ x = z$$

を充たす集合であること。また$commutativity$(可換性)は

$$\{y,z\}=\{z,y\}$$

であることを表しています。