:: deftheorem defines INT.Ring INT_3:def 12 :
for n being natural Number holds INT.Ring n = doubleLoopStr(# (Segm n),(addint n),(multint n),(In (1,(Segm n))),(In (0,(Segm n))) #);