let UN be Universe; :: thesis: for x being Element of GroupObjects UN holds x is strict AddGroup
let x be Element of GroupObjects UN; :: thesis: x is strict AddGroup
consider u being object such that
u in UN and
A1: GO u,x by Def22;
ex x1, x2, x3, x4 being set st
( u = [x1,x2,x3,x4] & ex G being strict AddGroup st
( x = G & x1 = the carrier of G & x2 = the addF of G & x3 = comp G & x4 = 0. G ) ) by A1;
hence x is strict AddGroup ; :: thesis: verum