:: deftheorem defines Initial_section BCIALG_4:def 10 :
for X being BCI-algebra
for a being Element of X holds Initial_section a = { t where t is Element of X : t <= a } ;