for x being set
for X being non empty constituted-DTrees set holds
( x in Subtrees X iff ex t being Element of X ex n being Node of t st x = t | n ) ;