for X being BCI-algebra
for a, b being Element of AtomSet X st a <> b holds
(BranchV a) /\ (BranchV b) = {}