let D be non empty set ; :: thesis: for T being DecoratedTree of D
for y being set st y in rng T holds
y is Element of D
let T be DecoratedTree of D; :: thesis: for y being set st y in rng T holds
y is Element of D
rng T c= D by TREES_2:def 9;
hence for y being set st y in rng T holds
y is Element of D ; :: thesis: verum