:: deftheorem defines BranchV BCIALG_1:def 17 :
for X being BCI-algebra
for a being Element of AtomSet X holds BranchV a = { x where x is Element of X : a <= x } ;