theorem Th2: :: BCIALG_2:2

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