theorem Th10: :: TREES_9:10

for x being set
for t being DecoratedTree holds
( x in Subtrees t iff ex n being Node of t st x = t | n ) ;