:: deftheorem defines associating MIDSP_2:def 2 :
for M being non empty MidStr
for G being non empty addLoopStr
for w being Function of [: the carrier of M, the carrier of M:], the carrier of G holds
( w is associating iff for p, q, r being Point of M holds
( p @ q = r iff w . (p,r) = w . (r,q) ) );