let i, j, m, n be 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:9;
then
n - i >= 1
by NAT_1:14;
then A4:
(n - i) + i >= 1
+ i
by XREAL_1:6;
m >= i
by A1, Th25;
then A5:
m + 1
>= i + 1
by XREAL_1:6;
(
j - i is
Element of
NAT &
j - i > i - i )
by A2, NAT_1:21, XREAL_1:9;
then
j - i >= 1
by NAT_1:14;
then A6:
(j - i) + i >= 1
+ i
by XREAL_1:6;
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:6;
(
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