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