xbool.0.miz

次に$xbool.0$を読み解いてみます。

まず,始めの環境部は

environ

 vocabulary TARSKI, BOOLE, ZFMISC_1;
 constructors TARSKI;
 notation TARSKI;
 theorems TARSKI;
 schemes TARSKI;

と書かれています。これは,

1. この$xbool.0$で使う用語($vocabulary$)が $TARSKI.voc, BOOLE,voc, ZFMISC_1.voc$というファイルに書かれていること。
2. $TARSIKI$
3. この$xbool.0$で既に証明済みとして引用する定理が $TARSIKI.abs$というファイルに書かれていること。
4. この$xbool.0$で引用する公理図式$schemes$が $TARSIKI.abs$というファイルに書かれていること。

を表しています。

 reserve X, Y, Z, x, y, z for set;

では $X, Y, Z, x, y, z$が任意の集合,すなわち,任意の変数であることを 宣言しています。

以下,$xbool.0$の本文が書かれています。