theorem BOOLE'46: :: BOOLE'46:

theorem BOOLE'46: :: BOOLE'46:
  X c= Y implies X \ Z c= Y \ Z
proof
  assume A1:X c= Y;
  let x;
  assume x in X \ Z;
  then x in X & not x in Z by XBOOLE_0:def 4;
  then x in Y & not x in Z by A1,TARSKI:def 3;
  hence thesis by XBOOLE_0:def 4;
end;

　これは以下の通りです。

$$X \subseteq Y \Rightarrow X \setminus Z \subseteq Y \setminus Z$$

証明　

$$\begin{eqnarray*}　 &&A1:X \subseteq Yを仮定し\\ &&xを任意にとり,さらに\\ ... ...BOOLE\_0:def 4から\\ &&X \setminus Z \subseteq Y \setminus Z \end{eqnarray*}$$

よって

$$X \subseteq Y \Rightarrow X \setminus Z \subseteq Y \setminus Z$$

証明終了