Mizar/本体部/関係演算子

成り立つ
A
A holds

A → B
A holds B

階層的に考えると{A{B}}
関数的に考えるとB(A)
Aという定義域が成立すると、Bという値域をもつ。

A ⇒ B
A implies B

A ⇔ B
A iff B

※if and only if ≡ iff