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
let x be set ; :: thesis: ( x in Z implies x is DecoratedTree of )
assume x in Z ; :: thesis: x is DecoratedTree of
hence x is DecoratedTree of by TARSKI:def 1; :: thesis: verum