theorem :: AMI_5'2 :

theorem :: AMI_5'2:
  X c= Y implies X c= Z \/ Y
 proof
  assume X c= Y; then
A1: Z \/ X c= Z \/ Y by BOOLE'33;
  X c= Z \/ X by BOOLE'31;
  hence X c= Z \/ Y by A1,BOOLE'29;
 end;

　これは以下の通りです。

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

証明

$$\begin{eqnarray*}　 &&X \subseteq Yを仮定するとBOOLE'33から\\ &&A1: Z \cup ... ... \cup X \\ &&よってA1,BOOLE'29から X \subseteq Z \cup Y \\ \end{eqnarray*}$$

証明終了