let X be non empty constituted-DTrees set ; :: thesis: X c= Subtrees X
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in Subtrees X )
assume x in X ; :: thesis: x in Subtrees X
then reconsider x = x as Element of X ;
reconsider p = {} as Element of dom x by TREES_1:22;
x = x | p by TREES_9:1;
hence x in Subtrees X ; :: thesis: verum