theorem :: BOOLE'45:

BOOLE'45: X \ Y = {} iff X c= Y
proof
  thus X \ Y = {} implies X c= Y
  proof
    assume A1:X \ Y = {};
    let x;
    assume x in X & not x in Y;
    then x in X \ Y by XBOOLE_0:def 4;
    hence contradiction by A1,XBOOLE_0:def 1;
  end;
  assume A2:X c= Y;
  now let x;
    x in X & not x in Y iff contradiction by A2,TARSKI:def 3;
    hence x in X \ Y iff x in {} by XBOOLE_0:def 4,def 1;
  end;
  hence thesis by TARSKI:2;
end;

　これは以下の通りです。

$$X \setminus Y = \{\} \Leftrightarrow X \subseteq Y$$

証明　

$$\begin{eqnarray*}　 &&先ず(1)~~ X \setminus Y = \{\} \Rightarrow X \subseteq Y... ...in \{\} \\ &&故にTARSKI:2から\\ &&X \setminus Y = \{\}\\ \end{eqnarray*}$$

よって

$$X \setminus Y = \{\} \Leftrightarrow X \subseteq Y$$

証明終了