Subtrees X c= Trees D

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Subtrees X or x in Trees D )
assume x in Subtrees X ; :: thesis: x in Trees D
then ex t being Element of X ex p being Node of t st x = t | p ;
hence x in Trees D by TREES_3:def 7; :: thesis: verum

end;

hence Subtrees X is non empty Subset of (Trees D) ; :: thesis: verum