theorem :: BCIALG_1:82

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