let i, j, m, n be Element of NAT ; :: thesis: for X being BCK-algebra of i,j,m,n st i <= m & i < n holds
X is BCK-algebra of i,j,i,i + 1
let X be BCK-algebra of i,j,m,n; :: thesis: ( i <= m & i < n implies X is BCK-algebra of i,j,i,i + 1 )
assume that
A1: i <= m and
A2: i < n ; :: thesis: X is BCK-algebra of i,j,i,i + 1
for x, y being Element of X holds Polynom i,j,x,y = Polynom i,(i + 1),y,x

proof

( n - i is Element of NAT & n - i > i - i ) by A2, NAT_1:21, XREAL_1:11;
then n - i >= 1 by NAT_1:14;
then A3: (n - i) + i >= 1 + i by XREAL_1:8;
let x, y be Element of X; :: thesis: Polynom i,j,x,y = Polynom i,(i + 1),y,x
A4: i + 1 < n + 1 by A2, XREAL_1:8;
A5: ( Polynom i,j,x,y = Polynom m,n,y,x & (y,(y \ x) to_power (m + 1)),(x \ y) to_power (i + 1) = (y,(y \ x) to_power (m + 1)),(x \ y) to_power (n + 1) ) by Def3, Th19;
( y,(y \ x) to_power (i + 1) = y,(y \ x) to_power (n + 1) & m + 1 >= i + 1 ) by A1, Th19, XREAL_1:8;
then y,(y \ x) to_power (i + 1) = y,(y \ x) to_power (m + 1) by A4, Th6;
hence Polynom i,j,x,y = Polynom i,(i + 1),y,x by A4, A5, A3, Th6; :: thesis: verum

end;

hence X is BCK-algebra of i,j,i,i + 1 by Def3; :: thesis: verum