let X be BCI-algebra; :: thesis: for a being Element of AtomSet X
for n being Nat st a is finite-period & ord a = n holds
a |^ n = 0. X
let a be Element of AtomSet X; :: thesis: for n being Nat st a is finite-period & ord a = n holds
a |^ n = 0. X
let n be Nat; :: thesis: ( a is finite-period & ord a = n implies a |^ n = 0. X )
assume ( a is finite-period & ord a = n ) ; :: thesis: a |^ n = 0. X
then a |^ n in BCK-part X by Def5;
then ex x being Element of X st
( x = a |^ n & 0. X <= x ) ;
then A1: (0. X) \ (a |^ n) = 0. X ;
a |^ n in AtomSet X by Th13;
then ex y being Element of X st
( y = a |^ n & y is atom ) ;
hence a |^ n = 0. X by A1; :: thesis: verum