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

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

証明　

$$\begin{eqnarray*}　 &&A1: Z \subseteq X ~and~ Z \subseteq Y　を仮定し， xを任... ...teq X ~and~ Z \subseteq Y \Rightarrow Z \subseteq X \cap Y \\ \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'39: :: BOOLE'39:
  Z c= X & Z c= Y implies Z c= X /\ Y
proof
  assume A1: [1] & Z c= Y;
  let x;
  assume [2];
  then x in X & x in Y by A1,[3]:def 3;
  hence thesis by [4]:def 3;
end;

　

    [選択肢]

[a]  XBOOLE_0
[b]  TARSKI
[c]  Z c= X
[d]  x in Z

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