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

$$X = Y \cap Z \Leftrightarrow X \subseteq Y ~and~ X \subse... ...eq Y ~and~ V \subseteq Z ) \Leftrightarrow ( V \subseteq X) )$$

証明　

$$\begin{eqnarray*}　 &&まず,BOOLE'37,BOOLE'39から\\ &&X = Y \cap Z \Rightarrow... ...Z \subseteq X \\ &&従ってBOOLE'37から Y \cap Z \subseteq X \\ \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'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 [1] implies
    X c= Y & X c= Z & for V st [2] 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= [3] implies V c= X;
  thus X c= Y /\ Z by BOOLE'39,A1,A2;
  Y /\ Z c= Y & [4] implies Y /\ Z c= X by A3;
  hence Y /\ Z c= X by BOOLE'37;
end;

　

    [選択肢]

[a]  Y /\ Z c= Z
[b]  V c= Y & V
[c]  X = Y /\ Z
[d]  Y & V c= Z

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