theorem :: BOOLE'34:

theorem :: BOOLE'34:
  X c= Y & Z c= V implies X \/ Z c= Y \/ V
proof
  assume A1: X c= Y;
  assume A2: Z c= V;
  let x; assume x in X \/ Z;
  then x in X or x in Z by XBOOLE_0:def 2;
  then x in Y or x in V by A1,A2,TARSKI:def 3;
  hence thesis by XBOOLE_0:def 2;
end;

　これは以下の通りです。

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

証明　

$$\begin{eqnarray*}　 &&A1: X \subseteq Y\\ &&A2: Z \subseteq V\\ &&を仮定... ...\in V \\ &&XBOOLE\_0:def 2から X \cup Z \subseteq Y \cup V \end{eqnarray*}$$

故に

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

証明終了