:: deftheorem Def20 defines associative BCIALG_1:def 20 :
for IT being BCI-algebra holds
( IT is associative iff for x, y, z being Element of IT holds (x \ y) \ z = x \ (y \ z) );