let S be non empty non void ManySortedSign ; :: thesis: for A being MSAlgebra over S holds A |= Equations (S,A)
let A be MSAlgebra over S; :: thesis: A |= Equations (S,A)
let s be SortSymbol of S; :: according to EQUATION:def 6 :: thesis: for b₁ being Element of (Equations S) . s holds
( not b₁ in (Equations (S,A)) . s or A |= b₁ )
let r be Element of (Equations S) . s; :: thesis: ( not r in (Equations (S,A)) . s or A |= r )
assume r in (Equations (S,A)) . s ; :: thesis: A |= r
then r in { e where e is Element of (Equations S) . s : A |= e } by Def14;
then consider e being Element of (Equations S) . s such that
A1: ( r = e & A |= e ) ;
thus A |= r by A1; :: thesis: verum