:: deftheorem defines quasi-commutative BCIALG_5:def 2 :
for X being BCI-algebra holds
( X is quasi-commutative iff ex i, j, m, n being Element of NAT st
for x, y being Element of X holds Polynom (i,j,x,y) = Polynom (m,n,y,x) );