theorem Th5: :: BCIALG_5:5

for m, n being Nat
for X being BCK-algebra
for x, y being Element of X st m >= n holds
(x,y) to_power m <= (x,y) to_power n