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