theorem BOOLE'40: :: BOOLE'40:

theorem BOOLE'40: :: BOOLE'40:
  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 & x in Z by XBOOLE_0:def 3;
  then x in Y & x in Z by A1,TARSKI:def 3;
  hence thesis by XBOOLE_0:def 3;
end;

　これは以下の通りです。

$$X \subseteq Y \Rightarrow X \cap Z \subseteq Y \cap Z$$

証明　

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

よって

$$X \subseteq Y \Rightarrow X \cap Z \subseteq Y \cap Z$$

証明終了