for S being locally_directed OrderSortedSign
for U1 being non-empty OSAlgebra of S
for R being OSCongruence of U1 holds
( OSNat_Hom (U1,R) is_epimorphism U1, QuotOSAlg (U1,R) & OSNat_Hom (U1,R) is order-sorted )