theorem :: SYSREL'2:

theorem :: SYSREL'2:
  (X \/ Y) \/ Z = (X \/ Z) \/ (Y \/ Z)
proof
  (X \/ Y) \/ Z = X \/ ((Z \/ Z) \/ Y) by BOOLE'64
            .= X \/ (Z \/ (Z \/ Y)) by BOOLE'64
            .= (X \/ Z) \/ (Y \/ Z) by BOOLE'64;
  hence thesis;
end;

　これは以下の通りです。

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

証明

$$\begin{eqnarray*}　 (X \cup Y) \cup Z &=& X \cup ((Z \cup Z) \cup Y)~~(BOOL... ...る）\\ &=& (X \cup Z) \cup (Y \cup Z)~~(BOOLE'64による）\\ \end{eqnarray*}$$

よって

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

証明終了