for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra over S
for E being EqualSet of S
for R being MSCongruence of U0 st U0 |= E holds
QuotMSAlg (U0,R) |= E by Th35;