theorem :: BCIALG_6:32

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