for t being DecoratedTree
for C being set holds
( C -Subtrees t is empty iff ( t is root & not t . {} in C ) )