theorem :: BCIALG_4:27

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