theorem :: BOOLE'59:

theorem :: BOOLE'59:
  X \/ Y = {} implies X = {}
proof
  assume
A1: X \/ Y = {};
  not ex x st x in X
  proof
    given x such that A3:x in X;
    x in X \/ Y by XBOOLE_0:def 2,A3;
    hence contradiction by A1,XBOOLE_0:def 1;
  end;
  hence thesis by XBOOLE_0:def 1;
end;

　これは以下の通りです。

$$X \cup Y = \{\} \Rightarrow X = \{\}$$

証明　

$$\begin{eqnarray*}　 &&A1: X \cup Y = \{\}を仮定すると\\ &&(1)~~not (\exists... ... &&これはA1とXBOOLE\_0:def 1から矛盾 \\ &&~~(1)の証明終了\\ \end{eqnarray*}$$

故に $XBOOLE\_0:def 1$により

$$X \cup Y = \{\} \Rightarrow X = \{\}$$

証明終了