theorem :: BOOLE'56:

theorem :: BOOLE'56:
  X = Y \/ Z iff Y c= X & Z c= X & for V st Y c= V & Z c= V holds X c= V
proof
  thus X = Y \/ Z implies
    Y c= X & Z c= X & for V st Y c= V & Z c= V holds X c= V
      by BOOLE'31,BOOLE'32;
  assume that A1: Y c= X and
              A2: Z c= X and
              A3: Y c= V & Z c= V implies X c= V;
  Y c= Y \/ Z & Z c= Y \/ Z by BOOLE'31;
  hence X c= Y \/ Z by A3;
  thus Y \/ Z c= X by A1,A2,BOOLE'32;
end;

　これは以下の通りです。

$$X = Y \cup Z \Leftrightarrow Y \subseteq X ~and~ Z \sub... ... (\forall V:Y \subseteq V ~and~ Z \subseteq V)(X \subseteq V)$$

証明　

$$\begin{eqnarray*}　 &&まず， BOOLE'31,BOOLE'32から\\ &&X = Y \cup Z \Righta... ...p Z \\ &&よって，A1,A2,BOOLE'32から Y \cup Z \subseteq X \\ \end{eqnarray*}$$

故に

$$X = Y \cup Z \Leftrightarrow Y \subseteq X ~and~ Z \sub... ... (\forall V:Y \subseteq V ~and~ Z \subseteq V)(X \subseteq V)$$

証明終了