theorem :: BCIALG_4:24

for X being BCI-Algebra_with_Condition(S)
for x being Element of X holds x |^ 3 = (x * x) * x