:: deftheorem defines initial_section BCIIDEAL:def 1 :
for X being BCI-algebra
for a being Element of X holds initial_section a = { x where x is Element of X : x <= a } ;