排他論理和

以下の記述は,集合$X$から$Y$の要素を除いた 差集合$X \setminus Y$と集合$Y$から$X$の要素を除いた 差集合$Y \setminus X$の和である排他論理和の集合を $X,Y$への作用($functor$) として定義しています。

 let Y be set;
 func X \+\ Y -> set equals
:Def6:  (X \ Y) \/ (Y \ X);
 correctness;
 commutativity;

文の冒頭の

 let Y be set;
 func X \+\ Y -> set equals
:Def6:  (X \ Y) \/ (Y \ X);

は$X,Y$の排他論理和の集合$X \oplus Y$が

$$X \setminus Y \cup Y \setminus X$$

と等しいものとして定義されます。 $X \oplus Y$は

X \ + \ Y

で表されています。

存在性は,既に,$X \setminus Y$も,$Y \setminus X$ も示されており,それの和集合

$$X \setminus Y \cup Y \setminus X$$

の存在も自明なので,

 correctness;

とだけ記述され省略されています。 また,

 commutativity;

は,$X$と$Y$を入れ替えても同じであることを示しています。 (可換性)