theorem Th35: :: BCIALG_1:35

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