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

$$(X \cup Y) \cup Z = X \cup (Y \cup Z)$$

証明

$$\begin{eqnarray*}　 &&まず，(1)~~(X \cup Y) \cup Z \subseteq X \cup (Y \cup Z)\... ...茲蝓\\ &&X \cup (Y \cup Z)　\subseteq　(X \cup Y) \cup Z \\ \end{eqnarray*}$$

よってこれと(1)から

$$(X \cup Y) \cup Z = X \cup (Y \cup Z)$$

証明終了

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'64: :: BOOLE'64:
  (X \/ Y) \/ Z = X \/ (Y \/ Z)
proof
 thus (X \/ Y) \/ Z c= X \/ (Y \/ Z)
   proof let x;
      assume [1] \/ Z;
      then x in X \/ Y or x in Z by XBOOLE_0:def 2;
      then [2] or x in Y or x in Z by XBOOLE_0:def 2;
      then x in X or x in [3] by XBOOLE_0:def 2;
      hence thesis by XBOOLE_0:def 2;
   end;
  let x;
  assume x in X \/ (Y \/ Z);
  then x in X or x in Y \/ Z by XBOOLE_0:def 2;
  then x in X or x in Y or x in Z by XBOOLE_0:def 2;
  then x in [4] or x in Z by XBOOLE_0:def 2;
  hence thesis by XBOOLE_0:def 2;
end;

    [選択肢]

[a]  x in (X \/ Y)
[b]  Y \/ Z
[c]  x in X
[d]  X \/ Y

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