for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for t being Term of S,X
for x being set st x in Subtrees t holds
x is Term of S,X