let S be non empty non void ManySortedSign ; :: thesis: for U0 being non-empty MSAlgebra of S
for E being EqualSet of S
for U2 being strict non-empty MSSubAlgebra of U0 st U0 |= E holds
U2 |= E
let U0 be non-empty MSAlgebra of S; :: thesis: for E being EqualSet of S
for U2 being strict non-empty MSSubAlgebra of U0 st U0 |= E holds
U2 |= E
let E be EqualSet of S; :: thesis: for U2 being strict non-empty MSSubAlgebra of U0 st U0 |= E holds
U2 |= E
let U2 be strict non-empty MSSubAlgebra of U0; :: thesis: ( U0 |= E implies U2 |= E )
assume A1: U0 |= E ; :: thesis: U2 |= 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
U2 |= e
let e be Element of (Equations S) . s; :: thesis: ( e in E . s implies U2 |= e )
assume e in E . s ; :: thesis: U2 |= e
then U0 |= e by A1, Def6;
hence U2 |= e by Th33; :: thesis: verum