theorem :: BCIALG_2:19

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