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

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