set p0 = the Node of t;
set S = { (t | p) where p is Node of t : verum } ;
t | the Node of t in { (t | p) where p is Node of t : verum } ;
then reconsider S = { (t | p) where p is Node of t : verum } as non empty set ;
S is constituted-DTrees

proof

let x be object ; :: according to TREES_3:def 5 :: thesis: ( not x in S or x is set )
assume x in S ; :: thesis: x is set
then ex p being Node of t st x = t | p ;
hence x is set ; :: thesis: verum

end;

hence ( Subtrees t is constituted-DTrees & not Subtrees t is empty ) ; :: thesis: verum