theorem Th26: :: BCIALG_6:26

for X being BCI-algebra
for a being Element of AtomSet X
for n being Nat st a is finite-period & ord a = n holds
a |^ n = 0. X