:: deftheorem defines X-1 FIELD_9:def 17 :
X-1 = <%(1. (Z/ 2)),(1. (Z/ 2))%>;