let X be BCI-algebra; :: thesis: for i, j, m, n being Element of NAT holds
( X is BCK-algebra of i,j,m,n iff X is BCK-algebra of m,n,i,j )
let i, j, m, n be Element of NAT ; :: thesis: ( X is BCK-algebra of i,j,m,n iff X is BCK-algebra of m,n,i,j )
thus
( X is BCK-algebra of i,j,m,n implies X is BCK-algebra of m,n,i,j )
:: thesis: ( X is BCK-algebra of m,n,i,j implies X is BCK-algebra of i,j,m,n )proof
assume A1:
X is
BCK-algebra of
i,
j,
m,
n
;
:: thesis: X is BCK-algebra of m,n,i,j
for
x,
y being
Element of
X holds
Polynom m,
n,
x,
y = Polynom i,
j,
y,
x
by A1, Def2;
hence
X is
BCK-algebra of
m,
n,
i,
j
by A1, Def2;
:: thesis: verum
end;
assume A1:
X is BCK-algebra of m,n,i,j
; :: thesis: X is BCK-algebra of i,j,m,n
for x, y being Element of X holds Polynom m,n,y,x = Polynom i,j,x,y
by A1, Def2;
hence
X is BCK-algebra of i,j,m,n
by A1, Def2; :: thesis: verum