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