基本的に定義、定理、仮定、結果それぞれから、式を満たすということを積み重ねて証明を行う。 定義、定理、仮定、結果はラベル名で示す。ラベル名は同じファイル内ならば、ラベル名のみで良いが、 違うファイルの場合には、

式 by ファイル名:ラベル番号;

で表し、式の後にby~と記す。 一つのラベルの指す処理から、一つの結果を表す場合には

式 by ラベル名;

n個のラベルの指す処理から、一つの結果を表す場合には

式 by ラベル名1,ラベル名2,...,ラベル名n;

となる

※このラベルで表さなければならない為にMizarで行う証明は正確であるが、Wikipediaにあるように、 「同等の内容を持つ通常の数学論文に比べ、長さにおいて4倍程度になると評価された」 と言われ、実際には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;