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 )

then A2: dom (x -tree (T1,T2)) is binary ;

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, Th8;

hence ( T1 is binary & T2 is binary ) ; :: thesis: verum

( ( 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
x -tree (T1,T2) is binary
; :: thesis: ( 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 ) ;

then A1: tree ((dom T1),(dom T2)) is binary by Th8;

dom (x -tree (T1,T2)) = tree ((dom T1),(dom T2)) by TREES_4:14;

hence x -tree (T1,T2) is binary by A1; :: thesis: verum

end;then ( dom T1 is binary & dom T2 is binary ) ;

then A1: tree ((dom T1),(dom T2)) is binary by Th8;

dom (x -tree (T1,T2)) = tree ((dom T1),(dom T2)) by TREES_4:14;

hence x -tree (T1,T2) is binary by A1; :: thesis: verum

then A2: dom (x -tree (T1,T2)) is binary ;

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, Th8;

hence ( T1 is binary & T2 is binary ) ; :: thesis: verum