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 )

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

( 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 m,n,i,j
; :: thesis: X is BCI-algebra of i,j,m,n
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;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

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