:: deftheorem Def12 defines HKOp BCIALG_6:def 12 :
for X being BCI-algebra
for G being SubAlgebra of X
for K being closed Ideal of X
for RK being I-congruence of X,K
for b₅ being BinOp of (Union (G,RK)) holds
( b₅ = HKOp (G,RK) iff for w1, w2 being Element of Union (G,RK)
for x, y being Element of X st w1 = x & w2 = y holds
b₅ . (w1,w2) = x \ y );