theorem Th7: :: CIRCTRM1:7

for X1, X2 being non empty constituted-DTrees set holds Subtrees (X1 \/ X2) = (Subtrees X1) \/ (Subtrees X2)