theorem :: BCIALG_1:81

for X being BCI-algebra
for x, y being Element of X st X is alternative holds
(x \ (x \ y)) \ (y \ x) = x