next up previous contents
: theorem BOOLE'33: :: BOOLE'33: : xboole1.miz : theorem BOOLE'31: :: BOOLE'31:   目次

theorem BOOLE'32: :: BOOLE'32: 

theorem BOOLE'32: :: BOOLE'32:
  X c= Z & Y c= Z implies X \/ Y c= Z
proof
  assume A1: X c= Z & Y c= Z;
  let x;
  assume x in X \/ Y;
  then x in X or x in Y by XBOOLE_0:def 2;
  hence thesis by  A1,TARSKI:def 3;
end;
　これは以下の通りです。

\begin{displaymath} X \subseteq Z ~and~ Y \subseteq Z \Rightarrow X \cup Y \subseteq Z \end{displaymath}

証明

\begin{eqnarray*}　 &&A1: X \subseteq Z ~and~ Y \subseteq Z\\ &&を仮定し，x... ...蠅垢襪�\\ &&XBOOLE\_0:def 2により， x \in X ~or~ x \in Y \\ \end{eqnarray*}

故に $A1,TARSKI:def 3$ から

\begin{displaymath} X \subseteq Z ~and~ Y \subseteq Z \Rightarrow X \cup Y \subseteq Z \end{displaymath}

証明終了


Yasunari SHIDAMA