theorem :: SYSREL'4:

theorem :: SYSREL'4:
  X c= Y /\ Z implies X c= Y
proof Y /\ Z c= Y by BOOLE'37;
  hence thesis by BOOLE'29;
end;

　これは以下の通りです。

$$X \subseteq Y \cap Z \Rightarrow X \subseteq Y$$

証明　

$$\begin{eqnarray*}　 &&BOOLE'37により，Y \cap Z \subseteq Y \\ &&故にBOOLE'29により\\ &&X \subseteq Y \cap Z \Rightarrow X \subseteq Y \\ \end{eqnarray*}$$

証明終了