theorem :: TREES_9:14

for x being set
for t being DecoratedTree holds
( x in FixedSubtrees t iff ex n being Node of t st x = [n,(t | n)] ) ;