theorem :: BCIALG_3:18

for X being BCI-algebra holds
( X is BCI-commutative iff for a being Element of AtomSet X
for x, y being Element of BranchV a holds x \ (x \ y) = y \ (y \ x) )