for X being BCI-algebra
for x being Element of X ex a being Element of AtomSet X st a <= x