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

hence ex b_{1} being BCI-algebra st

for x, y being Element of b_{1} holds Polynom (i,j,x,y) = Polynom (m,n,y,x)
; :: thesis: verum

hence ex b

for x, y being Element of b