theorem Th10: :: MSAFREE3:10

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