for S being non void Signature
for Y being V8() ManySortedSet of the carrier of S
for t being Term of S,Y
for p being Element of dom t holds variables_in (t | p) c= variables_in t