let X be BCI-algebra; :: thesis: for i, j, m, n being Element of NAT holds
( X is BCI-algebra of i,j,m,n iff X is BCI-algebra of m,n,i,j )
let i, j, m, n be Element of NAT ; :: thesis: ( X is BCI-algebra of i,j,m,n iff X is BCI-algebra of m,n,i,j )
thus ( X is BCI-algebra of i,j,m,n implies X is BCI-algebra of m,n,i,j ) :: thesis: ( X is BCI-algebra of m,n,i,j implies X is BCI-algebra of i,j,m,n )

proof

assume A1: X is BCI-algebra of i,j,m,n ; :: thesis: X is BCI-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 BCI-algebra of m,n,i,j by Def2; :: thesis: verum

end;

assume A1: X is BCI-algebra of m,n,i,j ; :: thesis: X is BCI-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 BCI-algebra of i,j,m,n by Def2; :: thesis: verum