for x, y being Element of BCI-EXAMPLE holds Polynom (i,j,x,y) = Polynom (m,n,y,x)
by STRUCT_0:def 10;

then reconsider B = BCI-EXAMPLE as BCI-algebra of i,j,m,n by Def3;

take B ; :: thesis: B is being_BCK-5

thus B is being_BCK-5 ; :: thesis: verum

then reconsider B = BCI-EXAMPLE as BCI-algebra of i,j,m,n by Def3;

take B ; :: thesis: B is being_BCK-5

thus B is being_BCK-5 ; :: thesis: verum