:: deftheorem defines having-inverse C0SP1:def 1 :
for V being non empty addLoopStr
for V1 being Subset of V holds
( V1 is having-inverse iff for v being Element of V st v in V1 holds
- v in V1 );