let X be BCI-algebra; :: thesis: 0. X in AtomSet X
for z being Element of X st z \ (0. X) = 0. X holds
z = 0. X by Th2;
then 0. X is atom ;
hence 0. X in AtomSet X ; :: thesis: verum