for S being ManySortedSign
for X being ManySortedSet of the carrier of S
for s, x being set holds
( ( x in X . s implies (X variables_in (root-tree [x,s])) . s = {x} ) & ( for s9 being set st ( s9 <> s or not x in X . s ) holds
(X variables_in (root-tree [x,s])) . s9 = {} ) )