theorem :: ABCMIZ_1:92

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