theorem BOOLE'35: :: BOOLE'35:

theorem BOOLE'35: :: BOOLE'35:
  X c= Y implies X \/ Y = Y
proof
  assume A1: X c= Y;
   thus X \/ Y c= Y
     proof
       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;
  let x;
  thus thesis by XBOOLE_0:def 2;
end;

　これは以下の通りです。

$$X \subseteq Y \Rightarrow X \cup Y = Y$$

証明　

$$\begin{eqnarray*}　 && A1: X \subseteq Yを仮定すると\\ &&まず(1)~~X \cup Y ... ... &&XBOOLE\_0:def 2により，x \in Y \Rightarrow x \in X \cup Y \end{eqnarray*}$$

ゆえに，

$$X \subseteq Y \Rightarrow X \cup Y = Y$$

証明終了