for U1 being Universal_Algebra
for E being Congruence of U1 holds Nat_Hom (U1,E) is_epimorphism