theorem :: BCIALG_6:33

for X being BCI-algebra
for x, y being Element of X
for a, b being Element of AtomSet X st a \ b is finite-period & x is finite-period & y is finite-period & a is finite-period & b is finite-period & x in BranchV a & y in BranchV b holds
ord (a \ b) divides (ord x) lcm (ord y)