let S be non empty non void ManySortedSign ; :: thesis: for U0 being non-empty MSAlgebra of S
for E being EqualSet of S
for R being MSCongruence of U0 st U0 |= E holds
QuotMSAlg U0,R |= E
let U0 be non-empty MSAlgebra of S; :: thesis: for E being EqualSet of S
for R being MSCongruence of U0 st U0 |= E holds
QuotMSAlg U0,R |= E
let E be EqualSet of S; :: thesis: for R being MSCongruence of U0 st U0 |= E holds
QuotMSAlg U0,R |= E
let R be MSCongruence of U0; :: thesis: ( U0 |= E implies QuotMSAlg U0,R |= E )
assume A1: U0 |= E ; :: thesis: QuotMSAlg U0,R |= E
let s be SortSymbol of S; :: according to EQUATION:def 6 :: thesis: for e being Element of (Equations S) . s st e in E . s holds
QuotMSAlg U0,R |= e
let e be Element of (Equations S) . s; :: thesis: ( e in E . s implies QuotMSAlg U0,R |= e )
assume e in E . s ; :: thesis: QuotMSAlg U0,R |= e
then U0 |= e by A1, Def6;
hence QuotMSAlg U0,R |= e by Th37; :: thesis: verum