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