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