theorem :: BCIALG_2:20

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