theorem Th15: :: TREES_3:15

for x, y being object holds
( {x,y} is constituted-Trees iff ( x is Tree & y is Tree ) )