theorem Th23: :: BCIALG_1:23

for X being BCI-algebra holds 0. X in AtomSet X