xboole1.miz

$TARSKI.miz$と$xboole0.miz$は集合論（$TARSKI$の公理系) についての公理と集合演算の定義が記述されていました。 $xboole1.miz$ではそれらを用いて，集合の基礎的な定理が展開されています。 ここではその一部を読み解くことにします。

ファイルの冒頭には，既に説明しましたように，『環境部』があります。

:: Boolean Properties of Sets - Theorems
::   Library Committee
::
:: Received April 08, 2002
:: Copyright (c) 2002 Association of Mizar Users

environ

 vocabulary BOOLE, ZFMISC_1;
 constructors TARSKI, XBOOLE_0;
 requirements BOOLE;
 notation TARSKI, XBOOLE_0;
 clusters XBOOLE_0;
 definitions TARSKI, XBOOLE_0;
 theorems TARSKI, XBOOLE_0;

begin

 reserve x,A,B,X,X',Y,Y',Z,V for set;

　

ここで使う記号法($vocabulary$)は$BOOLE.voc$と$ZFMISC\_1.voc$ に登録されています。

また，その記号法を用いた述語や用語$notation$は， $TARSKI, XBOOLE\_0$に記述されています。

それらの用語や記号を用いた定義$definitions$は $TARSKI, XBOOLE\_0$から引用され，定理$theorems$も 同様に $TARSKI, XBOOLE\_0$から引用されます。

以下，定理の記述を読んで行きます。