let X, Y be set ; :: thesis: ( X is constituted-DTrees & Y c= X implies Y is constituted-DTrees )
assume A1: for x being set st x in X holds
x is DecoratedTree ; :: according to TREES_3:def 5 :: thesis: ( not Y c= X or Y is constituted-DTrees )
assume A2: Y c= X ; :: thesis: Y is constituted-DTrees
let x be set ; :: according to TREES_3:def 5 :: thesis: ( x in Y implies x is DecoratedTree )
assume x in Y ; :: thesis: x is DecoratedTree
hence x is DecoratedTree by A1, A2; :: thesis: verum