Subtrees X c= FinTrees D

proof

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