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

$$X \subseteq Y \Rightarrow X \subseteq Z \cup Y$$

証明

$$\begin{eqnarray*}　 &&X \subseteq Yを仮定するとBOOLE'33から\\ &&A1: Z \cup X ... ... Z \cup X \\ &&よってA1,BOOLE'29から X \subseteq Z \cup 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 :: AMI_5'2:
  X c= Y implies X c= Z \/ Y
 proof
  assume [1]; then
A1: [2] c= [3] by BOOLE'33;
  [4] \/ X by BOOLE'31;
  hence X c= Z \/ Y by A1,BOOLE'29;
 end;

    [選択肢]

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

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