let T1, T2 be DecoratedTree; :: thesis: for x being set holds
( ( T1 is binary & T2 is binary ) iff x -tree T1,T2 is binary )
let x be set ; :: thesis: ( ( T1 is binary & T2 is binary ) iff x -tree T1,T2 is binary )

hereby :: thesis: ( x -tree T1,T2 is binary implies ( T1 is binary & T2 is binary ) )

assume ( T1 is binary & T2 is binary ) ; :: thesis: x -tree T1,T2 is binary
then ( dom T1 is binary & dom T2 is binary ) by Def3;
then A1: tree (dom T1),(dom T2) is binary by Th10;
dom (x -tree T1,T2) = tree (dom T1),(dom T2) by TREES_4:14;
hence x -tree T1,T2 is binary by A1, Def3; :: thesis: verum

end;

assume x -tree T1,T2 is binary ; :: thesis: ( T1 is binary & T2 is binary )
then A2: dom (x -tree T1,T2) is binary by Def3;
dom (x -tree T1,T2) = tree (dom T1),(dom T2) by TREES_4:14;
then ( dom T1 is binary & dom T2 is binary ) by A2, Th10;
hence ( T1 is binary & T2 is binary ) by Def3; :: thesis: verum