theorem :: BCIALG_2:21

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