証明の形式、骨組み：(スケルトン)
[論理式] proof [証明法] end;
 Aが成立する
 --------------------------------------------------
 proof
  thus A;
 end;
 Q⇒A
  Qを仮定する
   ～
  Aとなる
 --------------------------------------------------
 Q implies A
 proof
  assume Q;
   ～
  thus A;
 end;
 given = assume+ consider とする場合
 ((∃x)Q[x})⇒A
  xをQ[x}に与える
   ～
 Aとなる
 --------------------------------------------------
 (ex x st Q[x]) implies A
  proof
   given x such that Q[x];
   ······
   ～
   ······
   thus A;
  end;
 A⇔B
  A⇒B
  and
  B⇒A
 --------------------------------------------------
 A iff B
 proof
  thus A implies B;
  thus B implies A;
 end;
 A⇔B
  これにより
   Aを仮定
   Bとなる
  Bを仮定
  Aとなる
 --------------------------------------------------
 A iff B
 proof
  hereby
   assume A;
   thus B;
  end;
  assume B;
  thus A;
 end;
 A or B
 Aでないと仮定
 Bとなる
 ---------------------------------------------------
 A or B
 proof
  assume not A;
  thus B;
 end;
 A and B
 Aが成立
 Bが成立
 ---------------------------------------------------
 A & B
 proof
  thus A;
  thus B;
 end;
 ∀ x ∈集合  ⊆  f(x)
  x∈集合
  f(x)が成立
 ---------------------------------------------------
 for x being set holds f(x)
 proof
  let x be set;
  thus f(x);
 end;
 ∃ x ∈集合  ⇒  f(x)
  あるxとする
  f(x)が成立
 ---------------------------------------------------
 ex x being set st f(x)
 proof
  take a;
  thus f(a);
 end;
 Pは正しい
  Pは間違っていると仮定する
  矛盾する
 Qは間違っている
  Qは間違っていると仮定する
  矛盾しない
 A⇒B and B⇒C
 A⇒B or A⇒C
------------------------------------------------------------
------------------------------------------------------------
 consider 変数 型;
------------------------------------------------------------
変数rを再定義する場合には
 reconsider 変数 型;
------------------------------------------------------------
------------------------------------------------------------
ラベル付けを行う。(同じラベルの場合には直前のラベルが引用される)
 ラベル名:式;
 A1: a=b;
------------------------------------------------------------
that ラベル：式
such that ラベル：式
------------------------------------------------------------
------------------------------------------------------------
assume 仮定式
------------------------------------------------------------