:: deftheorem Def19 defines closed BCIALG_1:def 19 :
for X being BCI-algebra
for IT being Ideal of X holds
( IT is closed iff for x being Element of IT holds x ` in IT );