for Z being finite Tree
for o being Element of Z st o <> Root Z holds
card (Z | o) < card Z