let X be BCI-algebra; :: thesis: X is generated_by_atom
for x being Element of X ex a being Element of AtomSet X st a <= x by Th35;
hence X is generated_by_atom by Def16; :: thesis: verum