theorem Th25: :: BCIALG_6:25

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