:: deftheorem defines variables_in MSAFREE3:def 4 :
for S being non void Signature
for X being V8() ManySortedSet of the carrier of S
for t being Term of S,X holds variables_in t = S variables_in t;