theorem BOOLE'33: :: BOOLE'33:

theorem BOOLE'33: :: BOOLE'33:
  X c= Y implies X \/ Z c= Y \/ Z
proof
  assume A1: X c= Y;
  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 Z by A1,TARSKI:def 3;
  hence thesis by XBOOLE_0:def 2;
end;

　これは以下の通りです。

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

証明

$$\begin{eqnarray*}　 &&A1: X \subseteq Yを仮定し\\ &&xを任意にとり，さらに\\... ... \in Z \\ &&∴ A1,TARSKI:def 3によりx \in Y ~or~ x \in Z \\ \end{eqnarray*}$$

故に $XBOOLE\_0:def 2$から

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

証明終了