:: deftheorem defines GO GRCAT_1:def 23 :
for x, y being object holds
( GO x,y iff ex x1, x2, x3, x4 being set st
( x = [x1,x2,x3,x4] & ex G being strict AddGroup st
( y = G & x1 = the carrier of G & x2 = the addF of G & x3 = comp G & x4 = 0. G ) ) );