let X be BCI-algebra; :: thesis: for i, j, m, n being 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 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 X is BCI-algebra of i,j,m,n ; :: thesis: X is BCI-algebra of m,n,i,j
then for x, y being Element of X holds Polynom (m,n,x,y) = Polynom (i,j,y,x) by Def3;
hence X is BCI-algebra of m,n,i,j by Def3; :: thesis: verum

end;

assume X is BCI-algebra of m,n,i,j ; :: thesis: X is BCI-algebra of i,j,m,n
then for x, y being Element of X holds Polynom (m,n,y,x) = Polynom (i,j,x,y) by Def3;
hence X is BCI-algebra of i,j,m,n by Def3; :: thesis: verum