theorem :: BOOLE'57:

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

　これは以下の通りです。

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

証明

$$\begin{eqnarray*} 　 &&まず,BOOLE'37,BOOLE'39から\\ &&X = Y \cap Z \Righta... ...\subseteq X \\ &&従ってBOOLE'37から Y \cap Z \subseteq X \\ \end{eqnarray*}$$

証明終了