let D be non empty set ; :: thesis: FinTrees D c= Trees D
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in FinTrees D or x in Trees D )
assume x in FinTrees D ; :: thesis: x in Trees D
then x is DecoratedTree of D by Def6;
hence x in Trees D by Def7; :: thesis: verum