theorem :: BCIALG_6:6

for X being BCI-algebra
for x being Element of X holds x |^ 2 = x \ (x `)