定理$SYSREL'1$

以下は

$$\begin{eqnarray*} &&((X と Yが交わない) \ and \ ( x \in X \cap Y)) \\ && \Rig... ...X \ and \ not (x \in Y))\ or \ (x \in Y \ and \ not (x \in X))) \end{eqnarray*}$$

を表す定理です。

theorem :: SYSREL'1:
  X misses Y & x in X \/ Y implies
    ((x in X & not x in Y) or (x in Y & not x in X))
      by Def2,BOOLE'1;