述語論理記法で表記する
 域 演算
 性質
 proof
  ....
定義式
記号
 ∀x ∃y f(x)=a  → g(x)=h(y)
 -----------------------------------------------------------------
 理解しやすいように括弧でくくると
 ((∀x)(∃y)) (f(x)=a  → g(x)=h(y))
 -----------------------------------------------------------------
 関係式をより分かりやすくする
 ((∀x)(∃y))∋(f(x)=a  → g(x)=h(y))
 -----------------------------------------------------------------
 Mizarの述語論理記法
 for x ex y st f[x]=a holds g[x]=h[x];
 -----------------------------------------------------------------
 以上の要領で以下のようにも記述できる
 ∀x,y ∃t  x(t)⇔y(t)
 for x,y  ex t st x(t) iff y(t)
---------------------------------------------------------------------
 数学記号  記号名  Mizar  意味 
 ∀  全称記号  for (for, any)広がりを持った空間
 ∃  存在記号  ex  (existence , being)限定された空間(点など)
 →,⊂,⊆    holds  成り立つと 
 ∧  and  &  かつ 
 ∨  or  or  または 
  ￢  not  not  でない 
  ＝  =  =  等しい 
  ⇔  同値  iff  if and only if 
  ⇒  ならば  implies  ならば 
  ∈    <-   
  ：，∈    such that   
  ⊆    c=   
数学証明