:: deftheorem Def2 defines variables_in MSAFREE3:def 2 :
for S being ManySortedSign
for t being non empty Relation
for b₃ being ManySortedSet of the carrier of S holds
( b₃ = S variables_in t iff for s being object st s in the carrier of S holds
b₃ . s = { (a `1) where a is Element of rng t : a `2 = s } );