⇔
A means B;
定義中のラベルは :~: で表す。
※abstractファイルを作る場合には、 定義のラベルは
定理のラベルは
となります。
と等しい≡
y equals :ラベル名: 2*x;
置く⇒
x*y -> set means :A2: z;
正の値をもつ
x is positive means :A3: 0<x;
置換