:: deftheorem defines atom BCIALG_1:def 14 :
for X being BCI-algebra
for IT being Element of X holds
( IT is atom iff for z being Element of X st z \ IT = 0. X holds
z = IT );