for X being BCI-algebra
for x being Element of X
for a being Element of AtomSet X st x is finite-period & a is finite-period & x in BranchV a holds
ord x = ord a