for X being BCI-Algebra_with_Condition(S)
for a, b being Element of AtomSet X
for ma being Element of X st ( for x being Element of BranchV a holds x <= ma ) holds
ex mb being Element of X st
for y being Element of BranchV b holds y <= mb