let t be DecoratedTree; :: thesis: for X being non empty constituted-DTrees set st t in X holds
t in Subtrees X
let X be non empty constituted-DTrees set ; :: thesis: ( t in X implies t in Subtrees X )
assume t in X ; :: thesis: t in Subtrees X
then reconsider t = t as Element of X ;
reconsider e = {} as Node of t by TREES_1:22;
t | e = t by Th1;
hence t in Subtrees X ; :: thesis: verum