let X be BCI-Algebra_with_Condition(S); :: thesis: for x, a being Element of X holds ((x \ a) \ a) \ a = x \ (a |^ 3)
let x, a be Element of X; :: thesis: ((x \ a) \ a) \ a = x \ (a |^ 3)
(x \ a) \ a = x \ (a * a) by Th11;
then ((x \ a) \ a) \ a = x \ ((a * a) * a) by Th11
.= x \ ((a |^ 2) * a) by Th22
.= x \ (a |^ (2 + 1)) by Def6 ;
hence ((x \ a) \ a) \ a = x \ (a |^ 3) ; :: thesis: verum