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