let J be non empty non void Signature; :: thesis: for T being MSAlgebra over J

for X being VariableSet of T holds X c= Union the Sorts of T

let T be MSAlgebra over J; :: thesis: for X being VariableSet of T holds X c= Union the Sorts of T

let X be VariableSet of T; :: thesis: X c= Union the Sorts of T

consider G being GeneratorSet of T such that

A1: X = Union G by Def8;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in Union the Sorts of T )

assume x in X ; :: thesis: x in Union the Sorts of T

then consider y being object such that

A2: ( y in dom G & x in G . y ) by A1, CARD_5:2;

y in the carrier of J by A2;

then A3: y in dom the Sorts of T by PARTFUN1:def 2;

G c= the Sorts of T by PBOOLE:def 18;

then G . y c= the Sorts of T . y by A2;

hence x in Union the Sorts of T by A2, A3, CARD_5:2; :: thesis: verum

for X being VariableSet of T holds X c= Union the Sorts of T

let T be MSAlgebra over J; :: thesis: for X being VariableSet of T holds X c= Union the Sorts of T

let X be VariableSet of T; :: thesis: X c= Union the Sorts of T

consider G being GeneratorSet of T such that

A1: X = Union G by Def8;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in Union the Sorts of T )

assume x in X ; :: thesis: x in Union the Sorts of T

then consider y being object such that

A2: ( y in dom G & x in G . y ) by A1, CARD_5:2;

y in the carrier of J by A2;

then A3: y in dom the Sorts of T by PARTFUN1:def 2;

G c= the Sorts of T by PBOOLE:def 18;

then G . y c= the Sorts of T . y by A2;

hence x in Union the Sorts of T by A2, A3, CARD_5:2; :: thesis: verum