theorem Th7: :: HILBERT2:7

for x being set
for T1, T2 being DecoratedTree holds
( (x -tree (T1,T2)) . <*0*> = T1 . {} & (x -tree (T1,T2)) . <*1*> = T2 . {} )