:: deftheorem defines Ker BCIALG_6:def 8 :
for X, X9 being BCI-algebra
for f being BCI-homomorphism of X,X9 holds Ker f = { x where x is Element of X : f . x = 0. X9 } ;