を証明していて，
を証明したわけではありません．両者のあいだには数学的距離があります.しかしこれは3章で説明したように環境部の definitions の中に TARSKI を書いておくことにより，システムが自動的に両者が同値であることを理解します．これは，TARSKI の abstract ファイル中に predicate (述語命題)としてこのことが定義されていることによります.
TARSKI には，Mizar ライブラリの基本となる定理から構成されているため，アーティクルを書くにあたっては環境部の definitions のところに TARSKI を書いておきます．