theorem BOOLE'71: :: BOOLE'71:

theorem BOOLE'71: :: BOOLE'71:
  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 or x in Y /\ Z by XBOOLE_0:def 2;
    then x in X or x in Y & x in Z by XBOOLE_0:def 3;
    then x in X \/ Y & x in X \/ Z by XBOOLE_0:def 2;
    hence thesis by XBOOLE_0:def 3;
  end;
  let x;
  assume x in (X \/ Y) /\ (X \/ Z);
   then x in X \/ Y & x in X \/ Z by XBOOLE_0:def 3;
   then (x in X or x in Y) & (x in X or x in Z) by XBOOLE_0:def 2;
   then x in X or x in Y /\ Z by XBOOLE_0:def 3;
  hence thesis by XBOOLE_0:def 2;
end;

　これは以下の通りです。

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

証明　

$$\begin{eqnarray*}　 &&先ず次が成り立つ \\ &&(1)~~X \cup Y \cap Z \subseteq ... ...\\ &&(X \cup Y) \cap (X \cup Z) \subseteq X \cup Y \cap Z\\ \end{eqnarray*}$$

証明終了