take {} ; :: thesis: for x being set st x in {} holds
x is DecoratedTree of
let x be set ; :: thesis: ( x in {} implies x is DecoratedTree of )
thus ( x in {} implies x is DecoratedTree of ) ; :: thesis: verum