theorem Th8: :: BINTREE1:8

for T1, T2 being Tree holds
( ( T1 is binary & T2 is binary ) iff tree (T1,T2) is binary )