for X being BCI-algebra
for a being Element of X
for x, b being Element of AtomSet X st x is Element of BranchV b holds
a \ x = a \ b