theorem Th3: :: TREES_3:3

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