for x, z being set
for S being ManySortedSign
for X being ManySortedSet of the carrier of S
for s being set st s in the carrier of S holds
for p being DTree-yielding FinSequence holds
( x in (X variables_in ([z, the carrier of S] -tree p)) . s iff ex t being DecoratedTree st
( t in rng p & x in (X variables_in t) . s ) )