theorem Th8: :: HILBERT2:8

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