:: deftheorem Def8 defines equ_kernel ALGSTR_4:def 8 :
for X, Y being set
for f being Function of X,Y
for b₄ being Equivalence_Relation of X holds
( b₄ = equ_kernel f iff for x, y being object holds
( [x,y] in b₄ iff ( x in X & y in X & f . x = f . y ) ) );