:: deftheorem Def13 defines IConSet BCIALG_2:def 13 :
for X being BCI-algebra
for b₂ being set holds
( b₂ = IConSet X iff for A1 being set holds
( A1 in b₂ iff ex I being Ideal of X st A1 is I-congruence of X,I ) );