for X being BCI-algebra
for a being Element of AtomSet X
for x being Element of BCK-part X holds a \ x = a