theorem Th17: :: BCIALG_3:17

for X being BCI-algebra holds
( X is BCI-commutative iff for x, y being Element of X holds (x \ (x \ y)) \ (y \ (y \ x)) = (0. X) \ (x \ y) )