集合$X$から$Y$の要素を除いた差集合$X \setminus Y$

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

  func X \ Y -> set means
:Def4:   x in it iff x in X & not x in Y;
  existence from Separation;
  uniqueness
   proof
    let A1, A2 be set such that
A10: x in A1 iff x in X & not x in Y and
A11: x in A2 iff x in X & not x in Y;
     now
      let x;
       x in A1 iff x in X & not x in Y by A10;
      hence x in A1 iff x in A2 by A11;
     end;
    hence A1 = A2 by TARSKI:2;
   end;
end;

文の冒頭の

  func X \ Y -> set means
:Def4:   x in it iff x in X & not x in Y;

は$X,Y$の差集合$X \setminus Y$が

$$x \in X \setminus Y \Leftrightarrow (x \in X \ and \ not (\ x \in Y))$$

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

X \ Y

で表されています。

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

  existence from Separation;

とだけ記述されます。

一意性の証明は

  uniqueness

の後に書かれています。

集合$A1, A2$が

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

かつ

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

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

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

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

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

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

$$A1 = A2$$

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