theorem :: BCIALG_2:8

for X being BCI-algebra
for x, y being Element of X
for n being Nat holds (x,(x \ (x \ y))) to_power n = (x,y) to_power n