for X being BCI-algebra
for A being Ideal of X
for a being Element of A holds initial_section a c= A