let X be BCI-algebra; :: thesis: for x, y being Element of X st X is alternative holds
y \ (y \ (x \ (x \ y))) = y
let x, y be Element of X; :: thesis: ( X is alternative implies y \ (y \ (x \ (x \ y))) = y )
assume X is alternative ; :: thesis: y \ (y \ (x \ (x \ y))) = y
then y \ (y \ (x \ (x \ y))) = y \ (y \ y) by Th76
.= y \ (0. X) by Def5
.= y by Th2 ;
hence y \ (y \ (x \ (x \ y))) = y ; :: thesis: verum