theorem :: BCIALG_3:21

for X being BCI-algebra holds
( X is BCI-commutative iff for x, y, z being Element of X st x <= y & x <= z holds
x <= y \ (y \ z) )