theorem Th12: :: TREES_3:12

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