theorem Th9: :: MSAFREE3:9

for S being ManySortedSign
for X being ManySortedSet of the carrier of S
for t being non empty Relation
for V being ManySortedSubset of X holds
( V = X variables_in t iff for s being set st s in the carrier of S holds
V . s = (X . s) /\ { (a `1) where a is Element of rng t : a `2 = s } )