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