theorem Th5: :: HILBERT2:5

for x being set
for T1, T2 being Tree holds
( <*x*> in tree (T1,T2) iff ( x = 0 or x = 1 ) )