theorem :: TREES_3:5

for X, Y being set st X is constituted-Trees holds
( X /\ Y is constituted-Trees & Y /\ X is constituted-Trees & X \ Y is constituted-Trees )