theorem Th6: :: HILBERT2:6

for x being set
for T1, T2 being DecoratedTree holds (x -tree (T1,T2)) . {} = x