let n be Element of 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 )
B1: (x \ y) \ x = (x \ x) \ y by BCIALG_1:7
.= y ` by BCIALG_1:def 5
.= 0. X by BCIALG_1:def 8 ;
((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 (x,y to_power n) \ y <= x,y to_power n by BCIALG_1:def 11;
hence ( x \ y <= x & x,y to_power (n + 1) <= x,y to_power n ) by B1, BCIALG_1:def 11, BCIALG_2:4; :: thesis: verum