基本的に定義、定理、仮定、結果それぞれから、式を満たすということを積み重ねて証明を行う。 定義、定理、仮定、結果はラベル名で示す。ラベル名は同じファイル内ならば、ラベル名のみで良いが、 違うファイルの場合には、
式 by ファイル名:ラベル番号;
で表し、式の後にby～と記す。 一つのラベルの指す処理から、一つの結果を表す場合には
式 by ラベル名;
n個のラベルの指す処理から、一つの結果を表す場合には
式 by ラベル名1,ラベル名2,...,ラベル名n;
となる
※このラベルで表さなければならない為にMizarで行う証明は正確であるが、Wikipediaにあるように、 「同等の内容を持つ通常の数学論文に比べ、長さにおいて4倍程度になると評価された」 と言われ、実際には４倍以上手間がかかってしまう。
then consider X being 型 such that ... ラベルA:式 ... thus theis by ラベルA; end;
reserve X for Element of 型; reserve X for 型;
型の再定義 reconsider X as 型
a = b .= c; は以下と同等である a = b; then b=c;