let n be Nat; :: thesis: for X being BCK-algebra
for x, y being Element of X holds
( x \ y <= x & (x,y) to_power (n + 1) <= (x,y) to_power n )
let X be BCK-algebra; :: thesis: for x, y being Element of X holds
( x \ y <= x & (x,y) to_power (n + 1) <= (x,y) to_power n )
let x, y be Element of X; :: thesis: ( x \ y <= x & (x,y) to_power (n + 1) <= (x,y) to_power n )
(((x,y) to_power n) \ y) \ ((x,y) to_power n) = (((x,y) to_power n) \ ((x,y) to_power n)) \ y by BCIALG_1:7
.= y ` by BCIALG_1:def 5
.= 0. X by BCIALG_1:def 8 ;
then A1: ((x,y) to_power n) \ y <= (x,y) to_power n ;
(x \ y) \ x = (x \ x) \ y by BCIALG_1:7
.= y ` by BCIALG_1:def 5
.= 0. X by BCIALG_1:def 8 ;
hence ( x \ y <= x & (x,y) to_power (n + 1) <= (x,y) to_power n ) by A1, BCIALG_2:4; :: thesis: verum