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