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

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