:: deftheorem defines - ALGSTR_0:def 14 :
for V being addLoopStr
for v, w being Element of V holds v - w = v + (- w);