:: deftheorem Def12 defines Cng ALG_1:def 12 :
for U1, U2 being Universal_Algebra
for f being Function of U1,U2 st f is_homomorphism holds
for b₄ being Congruence of U1 holds
( b₄ = Cng f iff for a, b being Element of U1 holds
( [a,b] in b₄ iff f . a = f . b ) );