簡単な証明。以下の証明は当然エラーが出ない。なお、A1はラベルである。
 environ
 begin
   for x,y being set st x = y holds y = x
 proof
  let x,y be set;
  assume
   A1: x = y;
  thus y = x by A1;
 end;
 数式記号  beginの中では  proofの中では 
∀ ～∈...  for ～ being ...  let ～ be ... 
 ～ ⇒  ～ holds  assume ～ 
⇒ ～ holds ～  thus ～ 
なぜ、このように表現するかはトートロジーを学べば理解できるようになる。
即ち、∀ x,y は削除出来て、また、
 A⇒B
とは
 ￢A ∨ B
を示す。