Subtrees t c= Trees D

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Subtrees t or x in Trees D )
assume x in Subtrees t ; :: thesis: x in Trees D
then 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 t is non empty Subset of (Trees D) ; :: thesis: verum