:: deftheorem defines -tree TREES_4:def 5 :
for x being object
for T being DecoratedTree holds x -tree T = x -tree <*T*>;