theorem Th9: :: BINTREE1:9

for T1, T2 being DecoratedTree
for x being set holds
( ( T1 is binary & T2 is binary ) iff x -tree (T1,T2) is binary )