for X being non empty constituted-DTrees set holds Subtrees X = union { (Subtrees t) where t is Element of X : verum }