:: deftheorem defines INT.Group GR_CY_1:def 5 :
for n being non zero Nat holds INT.Group n = multMagma(# (Segm n),(addint n) #);