3.3.2　定理

　一般に本体部は定理と定義を中心にして構成されています．
　article で，定理を書くときには，

　　　　theorem　定理の式
　　　　proof
      ···
      ···
　　　　end:


と，書きます．
　こう書くのと先ほどの，

　　　　式
　　　　proof
      ···
      ···
　　　　end:


と，書くのではどう違うかというと，theorem と書くことによって，その式が abstract file に定理として抜きだされるということです．abstract file とは，article から theorem (定理の式) や definition (定義の式) などを抜きだしたファイルです．( .ABSファイル) article を，Miza rライブラリに登録するときには，article を abstract file にして登録します．なぜなら，証明などをすべて含んだ article ( .MIZファイル)では，ファイルの大きさが膨大になってしまって，そこから引用するものを見つけるのは大変だからです．ですから，引用してもらいたい式を書くときには theorem をつけておきます．
　article で定義を書くときには definition を使います．なにか新しい語を定義するとか，新しい関数を定義するときは，この definition を使って定義します．定義については後で詳しく説明します．
　それから，theorem や definition は proof 〜 end の中に書くことはできません．ネスティングの一番上の段階だけで使うことができます．つまり，

　　　　theorem　...
　　　 　proof
　　　　　theorem　...
　　　 　　proof
      ···
      ···
　　　　　end;
　　　　end;


と書くことはできません.
　このように，Mizar article は，大きく分けて環境部と本体部からなり，本体部は通常いくつかの定義と定理から成り立っています．
　また，Mizar articleでは : : 以降はコメントになります．