set S = { (t | p) where p is Node of t : verum } ;
consider p0 being Node of t;
t | p0 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 set ; :: 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