:: deftheorem Def7 defines all_vars_including MSAFREE4:def 7 :
for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for A being b₂,b₁ -terms MSAlgebra over S holds
( A is all_vars_including iff FreeGen X is ManySortedSubset of the Sorts of A );