:: deftheorem Def17 defines EqClaOp BCIALG_2:def 17 :
for X being BCI-algebra
for E being Congruence of X
for b₃ being BinOp of (Class E) holds
( b₃ = EqClaOp E iff for W1, W2 being Element of Class E
for x, y being Element of X st W1 = Class (E,x) & W2 = Class (E,y) holds
b₃ . (W1,W2) = Class (E,(x \ y)) );