Mizar/本体部

begin

--------------------------------------

共通変数定義

reserve X, Y, Z, x, y, z for set;

--------------------------------------

定義をする

definition

定義式;

existence 証明式 proof ～ end;

uniqueness 証明式 proof ～ end;

end;

--------------------------------------

定理の証明を行う場合に付ける(absファイルで使えるようにするために必要)

theorem

証明したい式

proof

変数定義

証明

結果

end;

--------------------------------------