consider d being Element of D;
take Z = {((elementary_tree 0) --> d)}; :: thesis: for x being set st x in Z holds
x is DecoratedTree of D
let x be set ; :: thesis: ( x in Z implies x is DecoratedTree of D )
assume x in Z ; :: thesis: x is DecoratedTree of D
hence x is DecoratedTree of D by TARSKI:def 1; :: thesis: verum