theorem :: BOOLE'44:

theorem :: BOOLE'44:
  X c= Z implies X \/ Y /\ Z = (X \/ Y) /\ Z
proof assume
A1: X c= Z;
  thus X \/ Y /\ Z c= (X \/ Y) /\ 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 Z by A1,XBOOLE_0:def 2,TARSKI:def 3;
    hence thesis by XBOOLE_0:def 3;
  end;
  let x;
  assume x in (X \/ Y) /\ Z;
  then x in X \/ Y & x in Z by XBOOLE_0:def 3;
  then (x in X or x in Y) & x in Z by XBOOLE_0:def 2;
  then x in X & x in Z or x in Y /\ Z by XBOOLE_0:def 3;
  hence thesis by XBOOLE_0:def 2;
end;

　これは以下の通りです。

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

証明　

$$\begin{eqnarray*}　 &&A1: X \subseteq Zを仮定すると\\ &&(1)~~ X \cup Y \cap... ...OLE\_0:def 2から\\ &&(X \cup Y) \cap Z = X \cup Y \cap Z \\ \end{eqnarray*}$$

よって

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

証明終了