for x, y being Element of BCI-EXAMPLE holds Polynom (0,0,x,y) = Polynom (0,0,y,x) by STRUCT_0:def 10;
hence BCI-EXAMPLE is quasi-commutative by Def2; :: thesis: verum