:: deftheorem Def3 defines associative BCIIDEAL:def 3 :
for X being BCI-algebra
for IT being Ideal of X holds
( IT is associative iff ( 0. X in IT & ( for x, y, z being Element of X st x \ (y \ z) in IT & y \ z in IT holds
x in IT ) ) );