theorem :: BOOLE'90:

theorem :: BOOLE'90:
  X \ Y = Y \ X implies X = Y
proof
   assume A1: X \ Y = Y \ X;
   now let x;
    (x in X & not x in Y) iff x in Y \ X by XBOOLE_0:def 4,A1;
    hence x in X iff x in Y by XBOOLE_0:def 4;
   end;
 hence thesis by TARSKI:2;
end;

　これは以下の通りです。

$$X \setminus Y = Y \setminus X \Rightarrow X = Y$$

証明　

$$\begin{eqnarray*}　 &&A1: X \setminus Y = Y \setminus Xを仮定すると：\\ &&x... ...w x \in Y \\ &&故にTARSKI:2により\\ &&X \Rightarrow X = Y \end{eqnarray*}$$

よって,

$$X \setminus Y = Y \setminus X \Rightarrow X = Y$$

証明終了