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