theorem BOOLE'69: :: BOOLE'69:

theorem BOOLE'69: :: BOOLE'69:
  X \/ (X /\ Y) = X
proof
  thus X \/ (X /\ Y) c= X
  proof let x;
    assume x in X \/ (X /\ Y);
    then x in X or x in X /\ Y by XBOOLE_0:def 2;
    hence thesis by XBOOLE_0:def 3;
  end;
  let x;
  thus thesis by XBOOLE_0:def 2;
end;

　これは以下の通りです。

$$X \cup (X \cap Y) = X$$

証明　

$$\begin{eqnarray*}　 &&(1)~~X \cup (X \cap Y) \subseteq X \\ &&(1)~~の証明 \... ... 2から \\ && x \in X \Rightarrow x \in X \cup (X \cap Y)\\ \end{eqnarray*}$$

よって

$$X \cup (X \cap Y) = X$$

証明終了