theorem BOOLE'42: :: BOOLE'42:

theorem BOOLE'42: :: BOOLE'42:
  X c= Y implies X /\ Y = X
proof
  assume A1: X c= Y;
  thus X /\ Y c= X by BOOLE'37;
  let x;
  assume x in X;
  then x in X & x in Y by A1,TARSKI:def 3;
  hence thesis by XBOOLE_0:def 3;
end;

　これは以下の通りです。

$$X \subseteq Y \Rightarrow X \cap Y = X$$

証明　

$$\begin{eqnarray*}　 &&A1: X \subseteq Yを仮定すると,\\ &&BOOLE'37により X \... ...x \in Y \\ &&故にXBOOLE\_0:def 3からX \subseteq X \cap Y \\ \end{eqnarray*}$$

よって

$$X \subseteq Y \Rightarrow X \cap Y = X$$

証明終了