theorem Th8: :: PRE_CIRC:9

for T being finite Tree
for p being Element of T holds T | p, { t where t is Element of T : p is_a_prefix_of t } are_equipotent