theorem Th13: :: BCIALG_6:13

for X being BCI-algebra
for a being Element of AtomSet X
for i being Integer holds a |^ i in AtomSet X