let i, j, m, n be Element of NAT ; for X being BCK-algebra of i,j,m,n st i = min i,j,m,n & i < j & i < n holds
X is BCK-algebra of i,i + 1,i,i + 1
let X be BCK-algebra of i,j,m,n; ( i = min i,j,m,n & i < j & i < n implies X is BCK-algebra of i,i + 1,i,i + 1 )
assume A1:
i = min i,j,m,n
; ( not i < j or not i < n or X is BCK-algebra of i,i + 1,i,i + 1 )
assume that
A2:
i < j
and
A3:
i < n
; X is BCK-algebra of i,i + 1,i,i + 1
for x, y being Element of X holds Polynom i,(i + 1),x,y = Polynom i,(i + 1),y,x
proof
(
n - i is
Element of
NAT &
n - i > i - i )
by A3, NAT_1:21, XREAL_1:11;
then
n - i >= 1
by NAT_1:14;
then A4:
(n - i) + i >= 1
+ i
by XREAL_1:8;
m >= i
by A1, Th25;
then A5:
m + 1
>= i + 1
by XREAL_1:8;
(
j - i is
Element of
NAT &
j - i > i - i )
by A2, NAT_1:21, XREAL_1:11;
then
j - i >= 1
by NAT_1:14;
then A6:
(j - i) + i >= 1
+ i
by XREAL_1:8;
let x,
y be
Element of
X;
Polynom i,(i + 1),x,y = Polynom i,(i + 1),y,x
A7:
i + 1
< n + 1
by A3, XREAL_1:8;
y,
(y \ x) to_power (i + 1) = y,
(y \ x) to_power (n + 1)
by Th19;
then A8:
y,
(y \ x) to_power (i + 1) = y,
(y \ x) to_power (m + 1)
by A7, A5, Th6;
A9:
(
Polynom i,
j,
x,
y = Polynom m,
n,
y,
x &
(y,(y \ x) to_power (i + 1)),
(x \ y) to_power (i + 1) = (y,(y \ x) to_power (i + 1)),
(x \ y) to_power (n + 1) )
by Def3, Th19;
(x,(x \ y) to_power (i + 1)),
(y \ x) to_power (i + 1) = (x,(x \ y) to_power (i + 1)),
(y \ x) to_power (n + 1)
by Th19;
then
(x,(x \ y) to_power (i + 1)),
(y \ x) to_power (i + 1) = (x,(x \ y) to_power (i + 1)),
(y \ x) to_power j
by A7, A6, Th6;
hence
Polynom i,
(i + 1),
x,
y = Polynom i,
(i + 1),
y,
x
by A7, A8, A9, A4, Th6;
verum
end;
hence
X is BCK-algebra of i,i + 1,i,i + 1
by Def3; verum