Mizar/本体部/性質

予約語	意味	備考
existence	存在する。	mode,functor,clusterは必須
uniqueness	一意性。ユニーク。	functorは必須
consistency	整合性。
compatibility	互換性。
coherence	一致性。
symmetry	対称性。
asymmetry	非対称性。
correctness	自明。正当性。	existence + uniqueness なのでfunctorの場合明らかな場合に使う
involutiveness	縮退性。
projectivity	投影性。
commutativity	可換性。
idempotence	同一性、同置性。
reflexivity	再帰性。
irreflexivity	非再帰性。