theorem BOOLE'47: :: BOOLE'47:

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

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

　これは以下の通りです。

証明　

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

よって

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

証明終了