theorem :: BOOLE'72:

theorem :: BOOLE'72:
  (X /\ Y) \/ (Y /\ Z) \/ (Z /\ X) = (X \/ Y) /\ (Y \/ Z) /\ (Z \/ X)
proof
  thus X /\ Y \/ Y /\ Z \/ Z /\ X
        = (X /\ Y \/ Y /\ Z \/ Z) /\ (X /\ Y \/ Y /\ Z \/ X) by BOOLE'71
       .= (X /\ Y \/ (Y /\ Z \/ Z)) /\ (X /\ Y \/ Y /\ Z \/ X) by BOOLE'64
       .= (X /\ Y \/ Z) /\ (X /\ Y \/ Y /\ Z \/ X) by BOOLE'69
       .= (X /\ Y \/ Z) /\ (X /\ Y \/ X \/ Y /\ Z) by BOOLE'64
       .= (X /\ Y \/ Z) /\ (X \/ Y /\ Z) by BOOLE'69
       .= (X \/ Z) /\ (Y \/ Z) /\ (X \/ Y /\ Z) by BOOLE'71
       .= (X \/ Z) /\ (Y \/ Z) /\ ((X \/ Y) /\ (X \/ Z)) by BOOLE'71
       .= (X \/ Y) /\ ((Y \/ Z) /\ (X \/ Z) /\ (X \/ Z)) by BOOLE'67
       .= (X \/ Y) /\ ((Y \/ Z) /\ ((X \/ Z) /\ (X \/ Z))) by BOOLE'67
       .= (X \/ Y) /\ (Y \/ Z) /\ (Z \/ X) by BOOLE'67;
end;

　これは以下の通りです。

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

証明

$$\begin{eqnarray*}　 X \cap Y \cup Y \cap Z \cup Z \cap X &=& (X \cap Y \cup... ...&=& (X \cup Y) \cap (Y \cup Z) \cap (Z \cup X) ~~( BOOLE'67)\\ \end{eqnarray*}$$

証明終了