:: deftheorem Def12 defines I-congruence BCIALG_2:def 12 :
for X being BCI-algebra
for A being Ideal of X
for b₃ being Relation of X holds
( b₃ is I-congruence of X,A iff for x, y being Element of X holds
( [x,y] in b₃ iff ( x \ y in A & y \ x in A ) ) );