:: deftheorem Def11 defines R-congruence BCIALG_2:def 11 :
for X being BCI-algebra
for b₂ being Equivalence_Relation of X holds
( b₂ is R-congruence of X iff for x, y being Element of X st [x,y] in b₂ holds
for u being Element of X holds [(x \ u),(y \ u)] in b₂ );