theorem :: BCIALG_2:22

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