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