Subtrees t c= FinTrees D

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Subtrees t or x in FinTrees D )
assume x in Subtrees t ; :: thesis: x in FinTrees D
then ex p being Node of t st x = t | p ;
then reconsider x = x as finite DecoratedTree of D ;
dom x is finite ;
hence x in FinTrees D by TREES_3:def 8; :: thesis: verum

end;

hence Subtrees t is non empty Subset of (FinTrees D) ; :: thesis: verum