排他和の定理

以下は定理

$$(x \in X \oplus Y ) \Leftrightarrow not (x \in X \Leftrightarrow x \in Y)$$

の証明です。

theorem
  x in X \+\ Y iff not (x in X iff x in Y)
proof
  X \+\ Y = (X \ Y) \/ (Y \ X) by Def6;
  then x in X \+\ Y iff x in X \ Y or x in Y \ X by Def2;
  hence thesis by Def4;
end;

定義$Def6$により,

$$X \oplus Y = (X \setminus Y ) \cup (Y \setminus X)$$

が成り立ち,これから,

$$x \in X \oplus Y \Leftrightarrow x \in (X \setminus Y )\ or \ x \in (Y \setminus X)$$

が成り立ち,定義$Def4$により証明終了です。