theorem :: BCIALG_2:17

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