let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in Subtrees X ; :: thesis:
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:

end;