集合 $X,Y$ の共通部分 $X \cap Y$

以下の記述は,$X,Y$の共通部分$X \cap Y$を$X,Y$への作用($functor$) として定義しています。

文の冒頭の

  func X /\ Y -> set means
:Def3:   x in it iff x in X & x in Y;

は$X,Y$の共通部分$X \cap Y$が

$$x \in X \cap Y \Leftrightarrow (x \in X \ and \ x \in Y)$$

を充たすものとして定義されます。$X \cap Y$は

X /\ Y

で表されています。

存在性は,既にこのファイルで証明した 分出の公理$Separation$から直ぐに言えますので,

  existence from Separation;

とだけ記述されます。

一意性の証明は

  uniqueness

の後に書かれています。

集合$A1, A2$が

$$A8: x \in A1 \Leftrightarrow (x \in X \ and \ x \in Y)$$

かつ

$$A9: x \in A2 \Leftrightarrow (x \in X \ and \ x \in Y)$$

を充たすものとします。このとき, $x$を任意にとると,$A8$により,

$$x \in A1 \Leftrightarrow (x \in X \ and \ x \in Y)$$

であり,これから,$A9$により,

$$x \in A1 \Leftrightarrow x \in A2$$

となります。従って,$TARSKI:2$に書かれている定理によって

$$A1 = A2$$

が成り立ち,一意性の証明が終了します。

  commutativity;
  idempotence;

は,$X,Y$の順序を替えた$Y \cap X$も同じものであり, $X=Y$の場合の$X \cap X$も定義されることを示しています。