:: deftheorem defines generated_by_atom BCIALG_1:def 16 :
for X being BCI-algebra holds
( X is generated_by_atom iff for x being Element of X ex a being Element of AtomSet X st a <= x );