:: deftheorem defines zeroEqC BCIALG_2:def 18 :
for X being BCI-algebra
for E being Congruence of X holds zeroEqC E = Class (E,(0. X));