let t be DecoratedTree; :: thesis: t in Subtrees t
reconsider e = {} as Node of t by TREES_1:22;
t | e = t by Th1;
hence t in Subtrees t ; :: thesis: verum