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