:: deftheorem Def9 defines Congruence BCIALG_2:def 9 :
for X being BCI-algebra
for b₂ being Equivalence_Relation of X holds
( b₂ is Congruence of X iff for x, y, u, v being Element of X st [x,y] in b₂ & [u,v] in b₂ holds
[(x \ u),(y \ v)] in b₂ );