for S being ManySortedSign
for o being set holds S variables_in ([o, the carrier of S] -tree {}) = EmptyMS the carrier of S