theorem :: BCIALG_3:20

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