:: deftheorem defines alternative BCIALG_1:def 27 :
for IT being BCI-algebra holds
( IT is alternative iff for x, y being Element of IT holds
( x \ (x \ y) = (x \ x) \ y & (x \ y) \ y = x \ (y \ y) ) );