:: deftheorem defines GO RINGCAT1:def 15 :
for x, y being object holds
( GO x,y iff ex x1, x2, x3, x4, x5, x6 being set st
( x = [[x1,x2,x3,x4],x5,x6] & ex G being strict Ring st
( y = G & x1 = the carrier of G & x2 = the addF of G & x3 = comp G & x4 = 0. G & x5 = the multF of G & x6 = 1. G ) ) );