theorem Th3: :: BCIALG_5:3

for n being Nat
for X being BCK-algebra
for x, y being Element of X holds
( x \ y <= x & (x,y) to_power (n + 1) <= (x,y) to_power n )