学籍番号::
名前::
以下の文章は命題の証明と、それをMizarで表したものである。
[ ]内の字句を埋め、Mizarのテキストを完成させて下さい。
解答は[1]〜[4]の順にアルファベットを続けて入力して下さい
証明
証明終了
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] X = Y /\ Z
[b] Y & V c= Z
[c] V c= Y & V
[d] Y /\ Z c= Z
[1]
[2]
[3]
[4]