theorem BOOLE'70: :: BOOLE'70:

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

　これは以下の通りです。

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

証明　

$$\begin{eqnarray*}　 &&先ず次が成り立つ \\ &&(1)~~ X \cap (Y \cup Z) \subset... ... \\ &&XBOOLE\_0:def 2から　x \in X ~and~ x \in Y \cup Z \\ \end{eqnarray*}$$

故に $XBOOLE\_0:def 3$と$(1)$から

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

証明終了