theorem Th1: :: BCIALG_6:1

for X being BCI-algebra
for x being Element of X
for a, b being Element of AtomSet X holds a \ (x \ b) = b \ (x \ a)