theorem Th96: :: ABCMIZ_1:96

for S being ManySortedSign
for o being set
for t1, t2 being DecoratedTree holds S variables_in ([o, the carrier of S] -tree <*t1,t2*>) = (S variables_in t1) (\/) (S variables_in t2)