theorem :: PRE_CIRC:16

for T being finite Tree
for p being Element of T st p <> {} holds
card (T | p) < card T