書き方
 集合論から全ての証明を行っているので、『A→B』 の証明をするには、以下の書き方をする
 environ
 
 begin
  for A,B being set st A holds B
 proof
  let A,B be set;
  assume A1: A;
  thus B by A1;
 end;
 証明のトートロジーより『A→B』と同値なものとして、『￢A∨B』が得られる。
この処理系では正しいことを『１』、正しくないことを『０』とします。
従って、処理系の内部では、上記の処理は以下の処理のように取り扱われる。
 {A,B⊂集合|A→B}
 証明
  A,B⊂集合
  ￢A ∨ B
型と書式の確認をした後で、
 A=1,B=1;
 not(A) and B;
の処理を行い。
 0 and 1
の結果は
 1
となり、正しいということになる。
だから、『assume』は英訳では仮定なのだが、Mizarの処理系では『not』となり、
『thus ～ by ラベル』 は 『ラベル and ～ 』となる。