:: deftheorem defines Z_2 BSPACE:def 2 :
Z_2 = INT.Ring 2;