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