:: deftheorem defines variables_in MSAFREE3:def 3 :
for S being ManySortedSign
for X being ManySortedSet of the carrier of S
for t being non empty Relation holds X variables_in t = X (/\) (S variables_in t);