Mizar/定義式

変数定義;
定義型 定義式;

性質
 proof
  ...
 end;