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