theorem :: SETWISEO'7:

theorem :: SETWISEO'7:
  X \/ Y c= Z implies X c= Z
proof
  X c= X \/ Y by BOOLE'31;
  hence thesis by BOOLE'29;
end;

　これは以下の通りです。

$$X \cup Y \subseteq Z \Rightarrow X \subseteq Z$$

証明

$$\begin{eqnarray*}　 &&BOOLE'31から，X \subseteq X \cup Y \\ &&故にBOOLE'29から\\ &&X \cup Y \subseteq Z \Rightarrow X \subseteq Z\\ \end{eqnarray*}$$

証明終了