:: deftheorem defines INT.Ring INT_3:def 3 :
INT.Ring = doubleLoopStr(# INT,addint,multint,(In (1,INT)),(In (0,INT)) #);