:: deftheorem defines `1 TREES_3:def 12 :
for D1, D2 being non empty set
for T being DecoratedTree of D1,D2 holds T `1 = (pr1 (D1,D2)) * T;