:: deftheorem defines additively-closed C0SP1:def 2 :
for V being non empty addLoopStr
for V1 being Subset of V holds
( V1 is additively-closed iff ( V1 is add-closed & V1 is having-inverse ) );