:: deftheorem defines |^ BCIALG_6:def 3 :
for X being BCI-algebra
for x being Element of X
for n being natural Number holds x |^ n = (BCI-power X) . (x,n);