3.2.4　definitions部

　definitions 部では，証明をする際の定義の拡張，証明の飛躍 (definitional expansion) を可能にしたい場合に，その定義がなされている article のファイル名を書きます．例えば，x c= y を証明するとき， ∀a(a in x implies a in Y) を証明すればよいのですが，この定義は article TARSKI の中に以下のように定義されています．

　　pred X c= Y means　x in X implies x in Y;

よって，definitions 部に TARSKI と書いておけば　x c= y を証明するとき，
a in x implies a in Y をいってしまえば x c= y が証明されたことになります．
　例，


　　　　　　theorem X c=X \/ Y
　　　　　　　proof let x be set;
　　　　　　　　　　　　assume　　x in X;
　　　　　　　　　　hence y in X \/ Y by BOOLE:def 2;
　　　　　　　　　　end: