:: deftheorem Def8 defines Variables MSATERM:def 8 :
for S being non empty non void ManySortedSign
for A being MSAlgebra over S
for b₃ being V2() ManySortedSet of the carrier of S holds
( b₃ is Variables of A iff b₃ misses the Sorts of A );