theorem :: BOOLE'41:

theorem :: BOOLE'41:
  X c= Y & Z c= V implies X /\ Z c= Y /\ V
proof
  assume A1: X c= Y & Z c= V;
  let x;
  assume x in X /\ Z;
  then x in X & x in Z by XBOOLE_0:def 3;
  then x in Y & x in V by A1,TARSKI:def 3;
  hence thesis by XBOOLE_0:def 3;
end;

　これは以下の通りです。

$$X \subseteq Y ~and~ Z \subseteq V \Rightarrow X \cap Z \subseteq Y \cap V$$

証明　

$$\begin{eqnarray*}　 &&次 A1: X \subseteq Y ~and~ Z \subseteq Vを仮定し,\\ &... ...&&故にXBOOLE\_0:def 3から\\ &&X \cap Z \subseteq Y \cap V\\ \end{eqnarray*}$$

よって

$$X \subseteq Y ~and~ Z \subseteq V \Rightarrow X \cap Z \subseteq Y \cap V$$

証明終了