set TT = union { (Funcs T,D) where T is Element of Trees : verum } ;
union { (Funcs T,D) where T is Element of Trees : verum } is constituted-DTrees

proof

let x be set ; :: according to TREES_3:def 5 :: thesis: ( x in union { (Funcs T,D) where T is Element of Trees : verum } implies x is DecoratedTree )
assume x in union { (Funcs T,D) where T is Element of Trees : verum } ; :: thesis: x is DecoratedTree
then consider X being set such that
A1: x in X and
A2: X in { (Funcs T,D) where T is Element of Trees : verum } by TARSKI:def 4;
ex T being Element of Trees st X = Funcs T,D by A2;
hence x is DecoratedTree by A1, Def6; :: thesis: verum

end;

then reconsider TT = union { (Funcs T,D) where T is Element of Trees : verum } as constituted-DTrees set ;
TT is DTree-set of D

proof

let x be set ; :: according to TREES_3:def 6 :: thesis: ( x in TT implies x is DecoratedTree of D )
assume x in TT ; :: thesis: x is DecoratedTree of D
then consider X being set such that
A3: x in X and
A4: X in { (Funcs T,D) where T is Element of Trees : verum } by TARSKI:def 4;
ex T being Element of Trees st X = Funcs T,D by A4;
hence x is DecoratedTree of D by A3, Def6; :: thesis: verum

end;

then reconsider TT = TT as DTree-set of D ;
take TT ; :: thesis: for T being DecoratedTree of D holds T in TT
let T be DecoratedTree of D; :: thesis: T in TT
reconsider t = dom T as Element of Trees by Def1;
rng T c= D by RELAT_1:def 19;
then A5: T in Funcs t,D by FUNCT_2:def 2;
Funcs t,D in { (Funcs W,D) where W is Element of Trees : verum } ;
hence T in TT by A5, TARSKI:def 4; :: thesis: verum