:: deftheorem defines AtomSet BCIALG_1:def 15 :
for X being BCI-algebra holds AtomSet X = { x where x is Element of X : x is atom } ;