let S be set ; :: thesis: ( S is empty implies ( S is constituted-Trees & S is constituted-FinTrees & S is constituted-DTrees ) )
assume A1: S is empty ; :: thesis: ( S is constituted-Trees & S is constituted-FinTrees & S is constituted-DTrees )
hence for x being set st x in S holds
x is Tree ; :: according to TREES_3:def 3 :: thesis: ( S is constituted-FinTrees & S is constituted-DTrees )
thus for x being set st x in S holds
x is finite Tree by A1; :: according to TREES_3:def 4 :: thesis: S is constituted-DTrees
thus for x being set st x in S holds
x is DecoratedTree by A1; :: according to TREES_3:def 5 :: thesis: verum