theorem :: BCIALG_6:31

for X being BCI-algebra
for x being Element of X st x is finite-period & x ` is finite-period holds
ord x = ord (x `)