theorem :: SYSREL'3:

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

　これは以下の通りです。

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

証明

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

故に

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

証明終了