set S = { (t | p) where t is Element of X, p is Node of t : verum } ;
consider t being Element of X, p0 being Node of t;
t | p0 in { (t | p) where t is Element of X, p is Node of t : verum } ;
then reconsider S = { (t | p) where t is Element of X, 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 t being Element of X ex p being Node of t st x = t | p ;
hence x is set ; :: thesis: verum

end;

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