学籍番号::
名前::
以下の文章は命題の証明と、それをMizarで表したものである。
$[~~]$内の字句を埋め、Mizarのテキストを完成させて下さい。
解答は[1]〜[4]の順にアルファベットを続けて入力して下さい

$$(X \cap Y) \cup (X \cap Z) \subseteq Y \cup Z$$

証明　

$$\begin{eqnarray*}　 　&&xを任意にとり, x \in (X \cap Y) \cup (X \cap Z)を仮定す... ...KI:def 3から\\ &&(X \cap Y) \cup (X \cap Z) \subseteq Y \cup Z \end{eqnarray*}$$

証明終了

environ

 vocabulary BOOLE, ZFMISC_1;
 notation TARSKI, XBOOLE_0;
 constructors TARSKI, XBOOLE_0;
 clusters XBOOLE_0;
 requirements BOOLE;
 
begin

 reserve x,A,B,X,X',Y,Y',Z,V for set;
 
theorem :: BOOLE'53:
  (X /\ Y) \/ (X /\ Z) c= Y \/ Z
proof
  now let x;
    assume x in ([1] /\ Y) \/ (X /\ Z);
    then x in ([2]) or x in (X /\ Z) by XBOOLE_0:def 2;
    then (x in X & x in Y) or (x in X & x in [3]) by XBOOLE_0:def 3;
    hence x in [4] by XBOOLE_0:def 2;
  end;
  hence thesis by TARSKI:def 3;
end;

    [選択肢]

[a]  Z
[b]  Y \/ Z
[c]  X /\ Y
[d]  X

[1] [2] [3] [4]