:: deftheorem defines - ALGSTR_2:def 2 :
for L being non empty left_add-cancelable add-right-invertible addLoopStr
for a, b being Element of L holds a - b = a + (- b);