L1: A=B by ...;
L2: B=C by ...;
L3: A=C by L1,L2;
ラベル 式 引用部
というふうに，その article中のラベルはそのまま，他の article からの引用の場合は，article名 : 数字です．また定義を引用する場合，article名 :def 数字です.
L3: A=C
proof
...
...
hence thesis;
end;
というふうに， proof 〜 end ではさんだいくつかの文で証明をつけることもできます．この場合，これ全体で１つの大きな文とみなせます．このとき，proof 〜 end の end の直前には thus もしくは hence という文を必要とします．これは，いま証明を付けている最初の式がこの文の式によっていえています，ということです．thus と hence の違いですが，hence は then + thus になっています．
then はここではじめて出てきましたが，直前の式を引用するときに使い，例で説明すると，
となっているとします．このときに，
と書く代わりに，L2 の式は直前の式ですから， L3 の文の引用部から L2 を取り除いて， thenを使って，
と書くことができます．
theorem 定理の式proof
...
...
end;
と，書きます．
式proof
...
...
end;
と，書くのではどう違うかというと，theorem と書くことによって，その式がabstract fileに定理として抜きだされるということです．abstract file とは，article から theorem （定理の式）や definition （定義の式）などを抜きだしたファイルです．（.ABS ファイル） article を，Mizar ライブラリに登録するときには，article を abstract file にして登録します．なぜなら，証明などをすべて含んだ article （.MIZ ファイル）では，ファイルの大きさが膨大になってしまって，そこから引用するものを見つけるのは大変だからです．ですから，引用してもらいたい式を書くときには theoremをつけておきます．
theorem ...proof
theorem ...
proof
...
...
end;
end;
と書くことはできません．