theorem Th30: :: GRCAT_1:30

for UN being Universe
for x being Element of GroupObjects UN holds x is strict AddGroup