theorem Th29: :: BCIALG_1:29

for X being BCI-algebra
for x being Element of X holds
( x in AtomSet X iff (x `) ` = x )