:: deftheorem defines zeroHK BCIALG_6:def 13 :
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 holds zeroHK (G,RK) = 0. X;