let m, n be Nat; :: thesis: for X being BCK-algebra
for x, y being Element of X st m >= n holds
(x,y) to_power m <= (x,y) to_power n
let X be BCK-algebra; :: thesis: for x, y being Element of X st m >= n holds
(x,y) to_power m <= (x,y) to_power n
let x, y be Element of X; :: thesis: ( m >= n implies (x,y) to_power m <= (x,y) to_power n )
assume m >= n ; :: thesis: (x,y) to_power m <= (x,y) to_power n
then m - n is Element of NAT by NAT_1:21;
then consider k being Element of NAT such that
A1: k = m - n ;
((x,y) to_power k) \ x = ((x \ x),y) to_power k by BCIALG_2:7
.= ((0. X),y) to_power k by BCIALG_1:def 5
.= 0. X by Th4 ;
then (x,y) to_power k <= x ;
then (((x,y) to_power k),y) to_power n <= (x,y) to_power n by BCIALG_2:19;
then (x,y) to_power (k + n) <= (x,y) to_power n by BCIALG_2:10;
hence (x,y) to_power m <= (x,y) to_power n by A1; :: thesis: verum