:: deftheorem defines X_ FIELD_9:def 16 :
X_ = <%(0. (Z/ 2)),(1. (Z/ 2))%>;