let x be set ; :: thesis: for T1, T2 being DecoratedTree holds (x -tree (T1,T2)) . {} = x
let T1, T2 be DecoratedTree; :: thesis: (x -tree (T1,T2)) . {} = x
x -tree (T1,T2) = x -tree <*T1,T2*> by TREES_4:def 6;
hence (x -tree (T1,T2)) . {} = x by TREES_4:def 4; :: thesis: verum