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