:: deftheorem defines / ALGSTR_1:def 11 :
for L being non empty almost_cancelable almost_invertible multLoopStr_0
for a, b being Element of L holds a / b = a * (b ");